charon_driver/translate/
translate_types.rs

1use itertools::Itertools;
2use rustc_middle::ty;
3use rustc_span::sym;
4use rustc_trait_elaboration::ItemId;
5use std::ops::ControlFlow;
6
7use super::translate_ctx::*;
8use crate::hax::{self, UnderOwnerState, Visibility};
9use charon_lib::ast::*;
10use charon_lib::ids::IndexVec;
11
12impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
13    pub(crate) fn translate_sized_proof(
14        &mut self,
15        span: Span,
16        ty: ty::Ty<'tcx>,
17    ) -> Result<Option<TraitRef>, Error> {
18        if self.options.hide_marker_traits {
19            return Ok(None);
20        }
21        let proof = hax::solve_sized(&self.hax_state, ty);
22        self.translate_trait_proof(span, &proof)
23            .map(PolyTraitRef::no_bound_vars)
24            .map(Some)
25    }
26
27    /// Translate an erased region. If we're inside a body, this will return a fresh body region
28    /// instead.
29    pub(crate) fn translate_erased_region(&mut self) -> Region {
30        if let Some(v) = &mut self.lifetime_freshener {
31            Region::Body(v.push(()))
32        } else {
33            Region::Erased
34        }
35    }
36
37    /// Generate a list of erased arguments, or fresh body lifetimes if we're inside a body.
38    pub(crate) fn translate_erased_region_args(&mut self, len: usize) -> RegionArgs {
39        RegionArgs::new((0..len).map(|_| self.translate_erased_region()).collect())
40    }
41
42    /// Erase a region binder by supplying erased lifetimes (or fresh body lifetimes) for all its
43    /// arguments.
44    pub(crate) fn erase_region_binder<T: TyVisitable>(&mut self, b: RegionBinder<T>) -> T {
45        let args = self.translate_erased_region_args(b.regions.len());
46        b.apply(args)
47    }
48
49    // Translate a region
50    pub(crate) fn translate_region(
51        &mut self,
52        span: Span,
53        region: &hax::Region,
54    ) -> Result<Region, Error> {
55        use crate::hax::RegionKind::*;
56        match &region.kind {
57            ReErased => Ok(self.translate_erased_region()),
58            ReStatic => Ok(Region::Static),
59            ReBound(hax::BoundVarIndexKind::Bound(id), br) => {
60                Ok(match self.lookup_bound_region(span, *id, br.var) {
61                    Ok(var) => Region::Var(var),
62                    Err(_) => Region::Erased,
63                })
64            }
65            ReEarlyParam(region) => Ok(match self.lookup_early_region(span, region) {
66                Ok(var) => Region::Var(var),
67                Err(_) => Region::Erased,
68            }),
69            ReLateParam(region) => Ok(Region::Var(self.lookup_late_param_region(span, region)?)),
70            RePlaceholder(placeholder) => {
71                // We use placeholders to track some closure regions that rustc erases.
72                for (dbid, level) in self.binding_levels.iter_enumerated() {
73                    if let Some(&rid) = level.closure_extra_self_regions.get(placeholder) {
74                        return Ok(Region::Var(DeBruijnVar::bound(dbid, rid)));
75                    }
76                }
77                if let hax::BoundRegionKind::NamedForPrinting(name) = placeholder.bound.kind
78                    && name.to_string().starts_with("__charon_closure_region_")
79                {
80                    return Ok(self.translate_erased_region());
81                }
82                raise_error!(self, span, "Unexpected placeholder region: {region:?}")
83            }
84            ReVar(..) => {
85                // Shouldn't exist outside of type inference.
86                raise_error!(
87                    self,
88                    span,
89                    "Should not exist outside of type inference: {region:?}"
90                )
91            }
92            ReBound(..) | ReError(..) => {
93                raise_error!(self, span, "Unexpected region kind: {region:?}")
94            }
95        }
96    }
97
98    pub(crate) fn translate_hax_int_ty(int_ty: &hax::IntTy) -> IntTy {
99        match int_ty {
100            hax::IntTy::Isize => IntTy::Isize,
101            hax::IntTy::I8 => IntTy::I8,
102            hax::IntTy::I16 => IntTy::I16,
103            hax::IntTy::I32 => IntTy::I32,
104            hax::IntTy::I64 => IntTy::I64,
105            hax::IntTy::I128 => IntTy::I128,
106        }
107    }
108
109    pub(crate) fn translate_hax_uint_ty(uint_ty: &hax::UintTy) -> UIntTy {
110        use crate::hax::UintTy;
111        match uint_ty {
112            UintTy::Usize => UIntTy::Usize,
113            UintTy::U8 => UIntTy::U8,
114            UintTy::U16 => UIntTy::U16,
115            UintTy::U32 => UIntTy::U32,
116            UintTy::U64 => UIntTy::U64,
117            UintTy::U128 => UIntTy::U128,
118        }
119    }
120
121    /// Translate a Ty.
122    ///
123    /// Typically used in this module to translate the fields of a structure/
124    /// enumeration definition, or later to translate the type of a variable.
125    ///
126    /// Note that we take as parameter a function to translate regions, because
127    /// regions can be translated in several manners (non-erased region or erased
128    /// regions), in which case the return type is different.
129    #[tracing::instrument(skip(self, span))]
130    pub(crate) fn translate_ty(&mut self, span: Span, hax_ty: &hax::Ty<'tcx>) -> Result<Ty, Error> {
131        let mut ty = if let Some(ty) = self
132            .innermost_binder()
133            .type_trans_cache
134            .get(hax_ty)
135            .cloned()
136        {
137            ty
138        } else {
139            let ty = self
140                .translate_ty_inner(span, hax_ty)
141                .unwrap_or_else(|e| TyKind::Error(e.msg).into_ty());
142            self.innermost_binder_mut()
143                .type_trans_cache
144                .insert(hax_ty.clone(), ty.clone());
145            ty
146        };
147        if let Some(v) = &mut self.lifetime_freshener {
148            // We might be reusing a value from cache: we must refresh the erased & body regions.
149            ty = ty.replace_erased_regions(|| Region::Body(v.push(())));
150        }
151        Ok(ty)
152    }
153
154    fn translate_ty_inner(&mut self, span: Span, ty: &hax::Ty<'tcx>) -> Result<Ty, Error> {
155        trace!("{:?}", ty);
156        let kind = match ty.kind() {
157            hax::TyKind::Bool => TyKind::Scalar(ScalarTy::Bool),
158            hax::TyKind::Char => TyKind::Scalar(ScalarTy::Char),
159            hax::TyKind::Int(int_ty) => TyKind::Scalar(ScalarTy::Integer(IntegerTy::Signed(
160                Self::translate_hax_int_ty(int_ty),
161            ))),
162            hax::TyKind::Uint(uint_ty) => TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(
163                Self::translate_hax_uint_ty(uint_ty),
164            ))),
165            hax::TyKind::Float(float_ty) => TyKind::Scalar(ScalarTy::Float(match float_ty {
166                hax::FloatTy::F16 => FloatTy::F16,
167                hax::FloatTy::F32 => FloatTy::F32,
168                hax::FloatTy::F64 => FloatTy::F64,
169                hax::FloatTy::F128 => FloatTy::F128,
170            })),
171            hax::TyKind::Never => TyKind::Never,
172
173            hax::TyKind::Alias(alias) => match &alias.kind {
174                hax::AliasKind::Projection(item) => {
175                    let trait_ref = self
176                        .translate_trait_proof(
177                            span,
178                            item.in_trait
179                                .as_ref()
180                                .expect("projection without a trait_ref?"),
181                        )?
182                        .erase();
183                    let assoc_type_id =
184                        self.translate_assoc_type_id(trait_ref.trait_id(), &item.def_id)?;
185                    let generics = self.translate_generic_args(span, item)?;
186                    TyKind::TraitType(trait_ref, assoc_type_id, generics)
187                }
188                hax::AliasKind::Opaque { hidden_ty, .. } => {
189                    return self.translate_ty(span, hidden_ty);
190                }
191                _ => {
192                    raise_error!(self, span, "Unsupported alias type: {:?}", alias.kind)
193                }
194            },
195
196            hax::TyKind::Adt(adt) => {
197                let tref = self.translate_type_decl_ref(span, &adt.item)?;
198                TyKind::Adt(tref)
199            }
200            hax::TyKind::Str(str_ty) => {
201                let tref = self.translate_type_decl_ref(span, &str_ty.item)?;
202                TyKind::Adt(tref)
203            }
204            hax::TyKind::Array(array) => {
205                let item_ref = &array.item;
206                let item_ty_is_sized = if let Some(proof) = array.element_sized_proof() {
207                    Some(self.translate_trait_proof(span, proof)?.no_bound_vars())
208                } else {
209                    None
210                };
211                let mut args = self.translate_generic_args_without_trait_refs(span, item_ref)?;
212                assert!(args.types.len() == 1 && args.const_generics.len() == 1);
213                TyKind::Array(
214                    args.types.pop().unwrap(),
215                    args.const_generics.pop().unwrap(),
216                    item_ty_is_sized,
217                )
218            }
219            hax::TyKind::Pat(pattern) => {
220                let ty = self.translate_ty(span, &pattern.ty)?;
221                let pat = self.translate_pattern(span, &pattern.pat)?;
222                TyKind::Pattern(ty, pat)
223            }
224            hax::TyKind::Slice(slice) => {
225                let item_ref = &slice.item;
226                let item_ty_is_sized = if let Some(proof) = slice.element_sized_proof() {
227                    Some(self.translate_trait_proof(span, proof)?.no_bound_vars())
228                } else {
229                    None
230                };
231                let mut args = self.translate_generic_args_without_trait_refs(span, item_ref)?;
232                assert!(args.types.len() == 1);
233                TyKind::Slice(args.types.pop().unwrap(), item_ty_is_sized)
234            }
235            hax::TyKind::Tuple(tuple) => {
236                let tref = self.translate_type_decl_ref(span, &tuple.item)?;
237                TyKind::Adt(tref)
238            }
239            hax::TyKind::Ref(reference) => {
240                trace!("Ref");
241
242                let region = self.translate_region(span, &reference.region)?;
243                let ty = self.translate_ty(span, &reference.ty)?;
244                let kind = if reference.mutbl.is_mut() {
245                    RefKind::Mut
246                } else {
247                    RefKind::Shared
248                };
249                TyKind::Ref(region, ty, kind)
250            }
251            hax::TyKind::RawPtr(ptr) => {
252                trace!("RawPtr: {:?}", (&ptr.ty, &ptr.mutbl));
253                let ty = self.translate_ty(span, &ptr.ty)?;
254                let kind = if ptr.mutbl.is_mut() {
255                    RefKind::Mut
256                } else {
257                    RefKind::Shared
258                };
259                TyKind::RawPtr(ty, kind)
260            }
261
262            hax::TyKind::Param(param) => {
263                // A type parameter, for example `T` in `fn f<T>(x : T) {}`.
264                match self.lookup_type_var(span, param) {
265                    Ok(ty) => ty.kind().clone(),
266                    Err(err) => TyKind::Error(err.msg),
267                }
268            }
269
270            hax::TyKind::Foreign(foreign) => {
271                let tref = self.translate_type_decl_ref(span, &foreign.item)?;
272                TyKind::Adt(tref)
273            }
274
275            hax::TyKind::FnPtr(fn_ptr) => {
276                trace!("FnPtr");
277                trace!("bound vars: {:?}", fn_ptr.sig.bound_vars);
278                let sig = self.translate_poly_fun_sig(span, &fn_ptr.sig)?;
279                TyKind::FnPtr(sig)
280            }
281            hax::TyKind::FnDef(fn_def) => {
282                let fnref =
283                    self.translate_bound_fn_ptr(span, &fn_def.item, TransItemSourceKind::Fun)?;
284                TyKind::FnDef(fnref)
285            }
286            hax::TyKind::Closure(args) => {
287                let tref = self.translate_closure_type_ref(span, &args.item)?;
288                TyKind::Adt(tref)
289            }
290
291            hax::TyKind::DynTrait(dyn_trait) => {
292                // self.check_no_monomorphize(span)?;
293                // Translate the region outside the binder.
294                let region = self.translate_region(span, &dyn_trait.region)?;
295
296                let binder =
297                    self.translate_dyn_binder(span, &dyn_trait.binder, |ctx, ty, ()| {
298                        let region = region.move_under_binder();
299                        ctx.innermost_binder_mut()
300                            .params
301                            .outlives
302                            .push(RegionBinder::empty(OutlivesPred(
303                                Region::Lub(ty.clone()),
304                                region,
305                            )));
306                        Ok(ty)
307                    })?;
308
309                if let Some(clause) = dyn_trait.principal_trait_clause()
310                    && let hax::ClauseKind::Trait(trait_predicate) = clause.hax_skip_binder_ref()
311                {
312                    // TODO(dyn): for now, we consider traits with associated types to not be dyn
313                    // compatible because we don't know how to handle them; for these we skip
314                    // translating the vtable.
315                    if self.trait_is_dyn_compatible(&trait_predicate.trait_ref.def_id) {
316                        // Ensure the vtable type is translated. The first predicate is the one that
317                        // can have methods, i.e. a vtable.
318                        let _: TypeDeclId = self.register_item(
319                            span,
320                            &trait_predicate.trait_ref,
321                            TransItemSourceKind::VTable,
322                        );
323                    }
324                }
325                TyKind::DynTrait(DynPredicate { binder })
326            }
327
328            hax::TyKind::Infer(_) => {
329                raise_error!(self, span, "Unsupported type: infer type")
330            }
331            hax::TyKind::Coroutine(..) => {
332                raise_error!(self, span, "Coroutine types are not supported yet")
333            }
334            hax::TyKind::Bound(_) => {
335                raise_error!(self, span, "Unexpected type kind: bound")
336            }
337            hax::TyKind::Placeholder(_) => {
338                raise_error!(self, span, "Unsupported type: placeholder")
339            }
340
341            hax::TyKind::Error => {
342                raise_error!(self, span, "Type checking error")
343            }
344            hax::TyKind::Todo(s) => {
345                raise_error!(self, span, "Unsupported type: {:?}", s)
346            }
347        };
348        Ok(kind.into_ty())
349    }
350
351    pub fn translate_pattern(
352        &mut self,
353        span: Span,
354        pat: &hax::Pattern<'tcx>,
355    ) -> Result<TypePattern, Error> {
356        Ok(match pat {
357            hax::Pattern::Range { start, end } => TypePattern::Range(
358                self.translate_constant_expr(span, start)?,
359                self.translate_constant_expr(span, end)?,
360            ),
361            hax::Pattern::Or(patterns) => TypePattern::OrPattern(
362                patterns
363                    .iter()
364                    .map(|pat| self.translate_pattern(span, pat))
365                    .try_collect()?,
366            ),
367            hax::Pattern::NotNull => TypePattern::NotNull,
368        })
369    }
370
371    pub(crate) fn translate_rustc_ty(
372        &mut self,
373        span: Span,
374        ty: &ty::Ty<'tcx>,
375    ) -> Result<Ty, Error> {
376        let ty = self.t_ctx.catch_sinto(&self.hax_state, span, ty)?;
377        self.translate_ty(span, &ty)
378    }
379
380    pub fn translate_poly_fun_sig(
381        &mut self,
382        span: Span,
383        sig: &hax::Binder<hax::TyFnSig<'tcx>>,
384    ) -> Result<RegionBinder<FunSig>, Error> {
385        self.translate_region_binder(span, sig, |ctx, sig| ctx.translate_fun_sig(span, sig))
386    }
387    pub fn translate_fun_sig(
388        &mut self,
389        span: Span,
390        sig: &hax::TyFnSig<'tcx>,
391    ) -> Result<FunSig, Error> {
392        let inputs = sig
393            .inputs
394            .iter()
395            .map(|x| self.translate_ty(span, x))
396            .try_collect()?;
397        let output = self.translate_ty(span, &sig.output)?;
398        Ok(FunSig {
399            is_unsafe: sig.safety == hax::Safety::Unsafe,
400            abi: Self::translate_abi(&sig.abi),
401            is_variadic: sig.c_variadic,
402            inputs,
403            output,
404        })
405    }
406
407    pub fn translate_abi(abi: &hax::ExternAbi) -> Abi {
408        match abi {
409            hax::ExternAbi::Rust => Abi::Rust,
410            hax::ExternAbi::C { unwind: false } => Abi::C,
411            _ => Abi::Other(abi.as_str().into()),
412        }
413    }
414
415    /// Translate an item's base generic arguments. This does not include extra arguments coming
416    /// from unerasing lifetimes or derived items; don't call directly; use `translate_xxx_ref` as
417    /// much as possible.
418    pub fn translate_generic_args(
419        &mut self,
420        span: Span,
421        item: &hax::ItemRef<'tcx>,
422    ) -> Result<GenericArgs, Error> {
423        self.translate_generic_args_inner(span, item, true)
424    }
425
426    /// Translate the same arguments without their trait proofs, e.g. for an instantiated name.
427    /// Don't call directly; use `translate_xxx_ref` as much as possible.
428    pub fn translate_generic_args_without_trait_refs(
429        &mut self,
430        span: Span,
431        item: &hax::ItemRef<'tcx>,
432    ) -> Result<GenericArgs, Error> {
433        self.translate_generic_args_inner(span, item, false)
434    }
435
436    fn translate_generic_args_inner(
437        &mut self,
438        span: Span,
439        item: &hax::ItemRef<'tcx>,
440        include_trait_refs: bool,
441    ) -> Result<GenericArgs, Error> {
442        // Items that have a typeck parent use their extra arguments for inference variables that
443        // we don't translate directly. Instead, use `translate_closure_region_args` to extract the
444        // arguments we do translate.
445        // FIXME: iterate through parents and find some uniform scheme
446        let substs = if let Some(parent) = item.def_id.typeck_parent(self.hax_state()) {
447            &item.generic_args[..parent.generics_of(self.hax_state()).count()]
448        } else {
449            &item.generic_args
450        };
451        let mut args = self.translate_raw_generic_args(span, substs)?;
452        if include_trait_refs {
453            args.trait_refs = self.translate_trait_proofs(span, &item.trait_proofs)?;
454        }
455        Ok(args)
456    }
457
458    /// Translate a raw list of generic arguments. This does not produce the arguments of a Charon
459    /// item: use `translate_generic_args` for item references.
460    fn translate_raw_generic_args(
461        &mut self,
462        span: Span,
463        substs: &[hax::GenericArg<'tcx>],
464    ) -> Result<GenericArgs, Error> {
465        let mut args = GenericArgs::empty();
466        for arg in substs {
467            match arg {
468                hax::GenericArg::Type(ty) => {
469                    args.types.push(self.translate_ty(span, ty)?);
470                }
471                hax::GenericArg::Lifetime(region) => {
472                    args.regions.push(self.translate_region(span, region)?);
473                }
474                hax::GenericArg::Const(c) => {
475                    args.const_generics
476                        .push(self.translate_constant_expr(span, c)?);
477                }
478            }
479        }
480        Ok(args)
481    }
482
483    /// In rustc/hax, closures and inline consts take a few extra generic types, which get inferred
484    /// and represent closure upvars and signature, or inline const return type. Instead of these
485    /// types, we add lifetime parameters. This method extracts the value of the lifetime
486    /// parameters in question.
487    // FIXME: iterate through parents, e.g. a promoted const in a closure needs these args provided,
488    // see `promoted-in-closure-regions.rs`. This is made harder by mono; we could streamline the
489    // whole thing by storing mono args inside the param defs, just like for inferred variables.
490    // Indeed the handling of inferred variables is pretty much a partial monomorphization. Maybe
491    // this would help with mono+traits.
492    pub(crate) fn recover_extra_early_regions(
493        &mut self,
494        span: Span,
495        item: &hax::ItemRef<'tcx>,
496    ) -> Result<Vec<Region>, Error> {
497        let def = self.poly_hax_def(&item.def_id)?;
498        let Some(param_env) = def.param_env() else {
499            return Ok(vec![]);
500        };
501        let num_regions = param_env.extra_early_regions.len();
502        if num_regions == 0 || self.options.monomorphize_with_hax {
503            return Ok((0..num_regions)
504                .map(|_| self.translate_erased_region())
505                .collect());
506        }
507        let actual = self.translate_raw_generic_args(span, &item.generic_args)?;
508
509        // We start from the original full args (with placeholder lifetimes), and
510        // instantiate+normalize them. This is crucial because the def may contain an associated
511        // type which has gotten normalized in `item`. Thankfully (I sure damn hope) going from
512        // erased to unerased lifetims can't make more normalization available, so this should
513        // guarantee that the types match structurally.
514        let template = hax::substitute(
515            self.tcx,
516            self.hax_state.typing_env(),
517            Some(item.rustc_args(self.hax_state())),
518            def.this().rustc_args(self.hax_state()),
519        );
520        let template: Vec<hax::GenericArg<'tcx>> = self.catch_sinto(span, &template)?;
521
522        // Translate the template arguments, with free regions instead of the placeholder ones.
523        let template = {
524            let template = self.inside_binder(BinderKind::Other, None, |this| {
525                let binder = this.innermost_binder_mut();
526                binder.is_hax_binder = false;
527                for region in &param_env.extra_early_regions {
528                    binder.push_unerased_region(region.clone());
529                }
530                this.translate_raw_generic_args(span, &template)
531            })?;
532            // Turn the regions we care about into `Free` regions.
533            let liberated_regions = template
534                .params
535                .regions
536                .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::Free(id)));
537            template.apply(&GenericArgs::new_lifetimes(liberated_regions))
538        };
539
540        struct RegionMapping {
541            args: charon_lib::ids::IndexVec<RegionId, Option<Region>>,
542            depth: DeBruijnId,
543        }
544        impl Visitor for RegionMapping {
545            type Break = ();
546        }
547        impl ZipAst for RegionMapping {
548            fn visit_region_param(&mut self, _: &RegionParam, _: &RegionParam) -> ControlFlow<()> {
549                ControlFlow::Continue(())
550            }
551
552            fn visit_region(&mut self, source: &Region, target: &Region) -> ControlFlow<()> {
553                if let (Region::Lub(source), Region::Lub(target)) = (source, target) {
554                    return self.visit(source, target);
555                }
556                if let Region::Var(DeBruijnVar::Free(id)) = *source
557                    && !matches!(target, Region::Erased | Region::Body(_))
558                {
559                    let Some(target) = target.clone().move_from_under_binders(self.depth) else {
560                        return ControlFlow::Break(());
561                    };
562                    let slot = &mut self.args[id];
563                    if slot.as_ref().is_none_or(|previous| *previous == target) {
564                        *slot = Some(target);
565                    } else {
566                        return ControlFlow::Break(());
567                    }
568                }
569                ControlFlow::Continue(())
570            }
571
572            fn visit_binder<T: AstVisitable>(
573                &mut self,
574                source: &Binder<T>,
575                target: &Binder<T>,
576            ) -> ControlFlow<()> {
577                self.depth = self.depth.incr();
578                let result = self.visit_inner(source, target);
579                self.depth = self.depth.decr();
580                result
581            }
582
583            fn visit_region_binder<T: AstVisitable>(
584                &mut self,
585                source: &RegionBinder<T>,
586                target: &RegionBinder<T>,
587            ) -> ControlFlow<()> {
588                self.depth = self.depth.incr();
589                let result = self.visit_inner(source, target);
590                self.depth = self.depth.decr();
591                result
592            }
593        }
594        let mut mapping = RegionMapping {
595            args: (0..num_regions).map(|_| None).collect(),
596            depth: DeBruijnId::zero(),
597        };
598        error_assert!(
599            self,
600            span,
601            ZipAst::visit(&mut mapping, &template, &actual).is_continue(),
602            "Inferred arguments don't match their definition: {:?} vs {:?}",
603            template,
604            actual
605        );
606        // Normalization may discard a parameter, for example through an associated type.
607        Ok(mapping
608            .args
609            .into_iter()
610            .map(|r| match r {
611                Some(r) => r,
612                None => self.translate_erased_region(),
613            })
614            .collect())
615    }
616
617    /// Whether Rust treats this type specially, i.e. whether it is a tuple, `str` or `Box`.
618    pub(crate) fn recognize_builtin_adt(
619        &mut self,
620        item: &hax::ItemRef<'tcx>,
621    ) -> Option<BuiltinAdt> {
622        item.def_id
623            .as_synthetic(self.hax_state())
624            .and_then(|synthetic| match synthetic {
625                hax::SyntheticItem::Tuple(_) => Some(BuiltinAdt::Tuple),
626                hax::SyntheticItem::Str => Some(BuiltinAdt::Str),
627                hax::SyntheticItem::Array
628                | hax::SyntheticItem::Slice
629                | hax::SyntheticItem::FnPtr(_) => None,
630            })
631            .or_else(|| {
632                (self.hax_def(item).ok()?.lang_item? == sym::owned_box).then_some(BuiltinAdt::Box)
633            })
634    }
635
636    /// Translate a Dynamically Sized Type metadata kind.
637    ///
638    /// Returns `None` if the type is generic, or if it is not a DST.
639    pub fn translate_ptr_metadata(
640        &mut self,
641        span: Span,
642        item: &hax::ItemRef<'tcx>,
643    ) -> Result<PtrMetadata, Error> {
644        // prepare the call to the method
645        use rustc_middle::ty;
646        let tcx = self.t_ctx.tcx;
647        let hax_state = &self.hax_state;
648        let ty_env = hax_state.typing_env();
649        let ty = item
650            .def_id
651            .type_of(hax_state)
652            .instantiate(tcx, item.rustc_args(hax_state));
653        let ty = hax::normalize(tcx, ty_env, ty);
654
655        // Get the tail type, which determines the metadata of `ty`.
656        let tail_ty = tcx.struct_tail_raw(
657            ty,
658            &rustc_middle::traits::ObligationCause::dummy(),
659            |ty| hax::normalize(tcx, ty_env, ty),
660            || {},
661        );
662        let hax_ty: hax::Ty<'tcx> = self.t_ctx.catch_sinto(hax_state, span, &tail_ty)?;
663
664        let ret = match tail_ty.kind() {
665            _ if tail_ty.is_sized(tcx, ty_env) => PtrMetadata::None,
666            ty::Str | ty::Slice(..) => PtrMetadata::Length,
667            ty::Dynamic(..) => match hax_ty.kind() {
668                hax::TyKind::DynTrait(dyn_trait) => {
669                    let principal_clause = dyn_trait
670                        .principal_trait_clause()
671                        .expect("expected a principal trait for vtable metadata");
672                    let vtable =
673                        self.translate_dyn_binder(span, &dyn_trait.binder, |ctx, _, _| {
674                            ctx.translate_region_binder(
675                                span,
676                                principal_clause,
677                                |ctx, kind: &hax::ClauseKind| {
678                                    let hax::ClauseKind::Trait(trait_predicate) = kind else {
679                                        unreachable!()
680                                    };
681                                    ctx.translate_vtable_struct_ref(
682                                        span,
683                                        &trait_predicate.trait_ref,
684                                    )
685                                },
686                            )
687                        })?;
688                    let vtable = vtable
689                        .skip_binder
690                        .try_substitute(&GenericArgs::empty())
691                        .expect("vtable struct should not depend on self type");
692                    let vtable = self.erase_region_binder(vtable);
693                    PtrMetadata::VTable(vtable)
694                }
695                _ => unreachable!("Unexpected hax type {hax_ty:?} for dynamic type: {ty:?}"),
696            },
697            // If we're hiding `Sized`, let's consider every param to be sized.
698            ty::Param(..) if self.t_ctx.options.hide_marker_traits => PtrMetadata::None,
699            ty::Param(..) => PtrMetadata::InheritFrom(self.translate_ty(span, &hax_ty)?),
700            ty::Placeholder(..) | ty::Infer(..) | ty::Bound(..) => {
701                panic!(
702                    "We should never encounter a placeholder, infer, or bound type from ptr_metadata translation. Got: {tail_ty:?}"
703                )
704            }
705            _ => PtrMetadata::None,
706        };
707
708        Ok(ret)
709    }
710
711    /// Translate a type layout.
712    ///
713    /// Translates the layout as queried from rustc into the more restricted [`Layout`].
714    #[tracing::instrument(skip(self))]
715    pub fn translate_layout(
716        &mut self,
717        span: Span,
718        def: &hax::FullDef<'tcx>,
719        kind: &TypeDeclKind,
720    ) -> Option<Layout> {
721        let item = def.this();
722        use rustc_abi as r_abi;
723
724        fn translate_variant_layout_data(
725            layout_data: &r_abi::LayoutData<r_abi::FieldIdx, r_abi::VariantIdx>,
726            inhabited: InhabitedPredicate,
727            tagger: Vec<(ByteCount, IntegerValue)>,
728        ) -> Option<VariantLayout> {
729            let field_offsets = match &layout_data.fields {
730                r_abi::FieldsShape::Arbitrary { offsets, .. } => {
731                    offsets.iter().map(|o| OffsetExpr::new(o.bytes())).collect()
732                }
733                r_abi::FieldsShape::Union(n) => (0..n.get()).map(|_| OffsetExpr::new(0)).collect(),
734                r_abi::FieldsShape::Primitive => IndexVec::default(),
735                r_abi::FieldsShape::Array { .. } => panic!("Unexpected layout shape"),
736            };
737            Some(VariantLayout {
738                field_offsets,
739                inhabited,
740                tagger,
741            })
742        }
743
744        fn translate_primitive_int(int_ty: r_abi::Integer, signed: bool) -> IntegerTy {
745            if signed {
746                IntegerTy::Signed(match int_ty {
747                    r_abi::Integer::I8 => IntTy::I8,
748                    r_abi::Integer::I16 => IntTy::I16,
749                    r_abi::Integer::I32 => IntTy::I32,
750                    r_abi::Integer::I64 => IntTy::I64,
751                    r_abi::Integer::I128 => IntTy::I128,
752                })
753            } else {
754                IntegerTy::Unsigned(match int_ty {
755                    r_abi::Integer::I8 => UIntTy::U8,
756                    r_abi::Integer::I16 => UIntTy::U16,
757                    r_abi::Integer::I32 => UIntTy::U32,
758                    r_abi::Integer::I64 => UIntTy::U64,
759                    r_abi::Integer::I128 => UIntTy::U128,
760                })
761            }
762        }
763
764        /// Returns expressions that compute the layout (size, align) chosen by rustc. For sized
765        /// types, that's plain integers; for unsized types, we build expressions that compute the
766        /// right value based on pointer metadata values. This mirrors rustc's
767        /// `size_and_align_of_dst` computation:
768        /// <https://github.com/rust-lang/rust/blob/3fbb92e14159dd8b9bdb81e065883d1132e5abb7/compiler/rustc_codegen_ssa/src/size_of_val.rs#L100-L182>.
769        fn chosen_size_and_align<'tcx>(
770            cx: &ty::layout::LayoutCx<'tcx>,
771            layout: ty::layout::TyAndLayout<'tcx>,
772        ) -> Option<(SizeExpr, SizeExpr)> {
773            let constant = |value: u64| SizeExprKind::from_usize(u128::from(value)).into_expr();
774
775            if layout.is_sized() {
776                return Some((
777                    constant(layout.size.bytes()),
778                    constant(layout.align.abi.bytes()),
779                ));
780            }
781
782            match layout.ty.kind() {
783                ty::Dynamic(..) => Some((
784                    SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
785                    SizeExprKind::FromMetadata(MetadataValue::DynAlign).into_expr(),
786                )),
787                ty::Slice(..) | ty::Str => {
788                    let unit = layout.field(cx, 0);
789                    Some((
790                        SizeExprKind::Scale(
791                            SizeExprKind::FromMetadata(MetadataValue::SliceLength).into_expr(),
792                            ConstantExpr::mk_usize(u128::from(unit.size.bytes())),
793                        )
794                        .into_expr(),
795                        constant(unit.align.abi.bytes()),
796                    ))
797                }
798                ty::Adt(..) | ty::Tuple(..) => {
799                    let tail_idx = layout.fields.count() - 1;
800                    let tail_offset = constant(layout.fields.offset(tail_idx).bytes());
801                    let sized_align = constant(layout.align.abi.bytes());
802                    let tail_layout = layout.field(cx, tail_idx);
803                    let (tail_size, mut tail_align) = chosen_size_and_align(cx, tail_layout)?;
804
805                    if let ty::Adt(def, _) = layout.ty.kind()
806                        && let Some(pack) = def.repr().pack
807                    {
808                        tail_align =
809                            SizeExprKind::Min(vec![tail_align, constant(pack.bytes())]).into_expr();
810                    }
811
812                    let full_align = SizeExprKind::Max(vec![sized_align, tail_align]).into_expr();
813                    let full_size = SizeExprKind::AlignTo {
814                        base: SizeExprKind::Plus(tail_offset, tail_size).into_expr(),
815                        target_align: full_align.clone(),
816                    }
817                    .into_expr();
818                    Some((full_size, full_align))
819                }
820                ty::Foreign(..) => None,
821                _ => None,
822            }
823        }
824
825        /// Marks the bytes of `layout` that aren't padding, i.e. that are part of a primitive in
826        /// at least one field of one variant. This mirrors MiniRust's `calc_chunks`:
827        /// <https://github.com/minirust/minirust/blob/master/tooling/minimize/src/chunks.rs>.
828        fn mark_data_bytes<'tcx>(
829            cx: &ty::layout::LayoutCx<'tcx>,
830            layout: ty::layout::TyAndLayout<'tcx>,
831            markers: &mut [bool],
832        ) {
833            // The tag of a multi-variant layout is handled as one of its fields below.
834            if let r_abi::Variants::Multiple { variants, .. } = &layout.variants {
835                for id in variants.indices() {
836                    mark_data_bytes(cx, layout.for_variant(cx, id), markers);
837                }
838            }
839            match layout.fields {
840                r_abi::FieldsShape::Primitive => markers[..layout.size.bytes_usize()].fill(true),
841                r_abi::FieldsShape::Array { stride, count } => {
842                    let elem = layout.field(cx, 0);
843                    // Skip ZSTs which may have huge counts ([(); isize::MAX] & co.)
844                    if elem.is_zst() {
845                        return;
846                    }
847                    let mut elem_markers = vec![false; elem.size.bytes_usize()];
848                    mark_data_bytes(cx, elem, &mut elem_markers);
849                    for i in 0..count {
850                        let offset = (stride * i).bytes_usize();
851                        for (m, e) in markers[offset..].iter_mut().zip(&elem_markers) {
852                            *m |= e;
853                        }
854                    }
855                }
856                r_abi::FieldsShape::Union(_) | r_abi::FieldsShape::Arbitrary { .. } => {
857                    for i in 0..layout.fields.count() {
858                        let offset = layout.fields.offset(i).bytes_usize();
859                        mark_data_bytes(cx, layout.field(cx, i), &mut markers[offset..]);
860                    }
861                }
862            }
863        }
864
865        let tcx = self.t_ctx.tcx;
866        let hax_state = self.hax_state_with_id();
867        assert_eq!(hax_state.owner(), item.def_id);
868        let ty_env = hax_state.typing_env();
869        let ty = item
870            .def_id
871            .type_of(hax_state)
872            .instantiate(tcx, item.rustc_args(hax_state));
873        let ty = hax::normalize(tcx, ty_env, ty);
874        let pseudo_input = ty_env.as_query_input(ty);
875        let ptr_size = self.translated.the_target_information().target_pointer_size;
876
877        let repr = match &def.kind {
878            hax::FullDefKind::Adt(adt) => self.translate_repr_options(adt.repr()),
879            _ => ReprOptions::default(),
880        };
881        let ty_layout = match tcx.layout_of(pseudo_input) {
882            Ok(layout) => layout,
883            Err(_) => return Layout::for_type(&self.translated, kind, repr),
884        };
885        let rustc_variant_inhabited = |id| match ty.kind() {
886            ty::Adt(adt, args) if adt.is_enum() => adt
887                .variant(id)
888                .inhabited_predicate(tcx)
889                .instantiate(tcx, args),
890            _ => ty.inhabited_predicate(tcx),
891        };
892        let inhabited = self
893            .translate_inhabited_predicate(span, ty.inhabited_predicate(tcx))
894            .ok()?;
895        let layout_cx = ty::layout::LayoutCx::new(tcx, ty_env);
896        let (size, align) = chosen_size_and_align(&layout_cx, ty_layout)?;
897        let size = Size::from_expr(size.normalize(Some(&self.translated), None, false));
898        let align = Size::from_expr(align.normalize(Some(&self.translated), None, false));
899        let layout = ty_layout.layout;
900
901        let num_variants = match kind {
902            TypeDeclKind::Struct(_) | TypeDeclKind::Union(_) => 1,
903            TypeDeclKind::Enum(variants) => variants.len(),
904            _ => match ty.variant_range(self.t_ctx.tcx) {
905                Some(range) => range.end.index(),
906                None => match layout.fields() {
907                    r_abi::FieldsShape::Arbitrary { .. } | r_abi::FieldsShape::Union(_) => 1,
908                    r_abi::FieldsShape::Primitive | r_abi::FieldsShape::Array { .. } => 0,
909                },
910            },
911        };
912        let mut variant_layouts: IndexVec<VariantId, Option<VariantLayout>> =
913            (0..num_variants).map(|_| None).collect();
914        // Build the discriminator tree and variant layouts.
915        let discriminator = match layout.variants() {
916            r_abi::Variants::Multiple {
917                tag,
918                tag_encoding,
919                tag_field,
920                variants,
921                ..
922            } => {
923                // The tag_field is the index into the `offsets` vector.
924                let r_abi::FieldsShape::Arbitrary { offsets, .. } = layout.fields() else {
925                    unreachable!()
926                };
927                let tag_offset = offsets
928                    .get(*tag_field)
929                    .map(|s| r_abi::Size::bytes(*s))
930                    .expect("No tag field offset for enum?");
931                let tag_offset_expr = OffsetExpr::new(tag_offset);
932
933                let tag_ty = match tag.primitive() {
934                    r_abi::Primitive::Int(int_ty, signed) => {
935                        translate_primitive_int(int_ty, signed)
936                    }
937                    r_abi::Primitive::Pointer(_) => IntegerTy::Signed(IntTy::Isize),
938                    r_abi::Primitive::Float(_) => unreachable!(),
939                };
940                let tag_size = r_abi::Size::from_bytes(tag_ty.target_size(ptr_size));
941                // Reinterpret raw tag bits in `tag_ty`, sign-extending if needed.
942                let tag_from_bits =
943                    |bits: u128| IntegerValue::from_bits(tag_ty, tag_size.truncate(bits));
944
945                struct VariantTagInfo {
946                    /// The value of the tag for this variant, even if this is the untagged variant
947                    /// of a niched enum. `None` if we can't compute it.
948                    value: Option<IntegerValue>,
949                    /// Whether the variant is inhabited or not.
950                    uninhabited: bool,
951                    /// Whether this is the niched (untagged) variant of a niched enum.
952                    niched: bool,
953                }
954                let taginfo_for_variant = |id: rustc_abi::VariantIdx| {
955                    let uninhabited = variants[id].is_uninhabited();
956                    match tag_encoding {
957                        r_abi::TagEncoding::Direct => {
958                            let value = if uninhabited {
959                                None
960                            } else {
961                                let tag = tcx
962                                    .tag_for_variant(ty_env.as_query_input((ty, id)))
963                                    .unwrap();
964                                Some(tag_from_bits(tag.to_bits(tag_size)))
965                            };
966                            VariantTagInfo {
967                                value,
968                                uninhabited,
969                                niched: false,
970                            }
971                        }
972                        r_abi::TagEncoding::Niche {
973                            untagged_variant,
974                            niche_variants,
975                            niche_start,
976                        } => {
977                            let value = niche_variants.contains(&id).then(|| {
978                                let relative = (id.index() - niche_variants.start.index()) as u128;
979                                tag_from_bits(niche_start.wrapping_add(relative))
980                            });
981                            VariantTagInfo {
982                                value,
983                                uninhabited,
984                                niched: id == *untagged_variant,
985                            }
986                        }
987                    }
988                };
989
990                // Compute per-variant tag values and build tagger + discriminator children.
991                let mut children = Vec::new();
992
993                for (id, variant_layout) in variants.iter_enumerated() {
994                    let variant_id = self.translate_variant_id(id);
995                    let taginfo = taginfo_for_variant(id);
996                    let variant_inhabited = self
997                        .translate_inhabited_predicate(span, rustc_variant_inhabited(id))
998                        .ok()?;
999                    let tagger = if let Some(val) = taginfo.value {
1000                        if taginfo.niched || taginfo.uninhabited {
1001                            // If we could compute a tag for this variant, encountering it is UB.
1002                            children.push((val..=val, Discriminator::Invalid));
1003                            vec![]
1004                        } else {
1005                            children.push((val..=val, Discriminator::Known(variant_id)));
1006                            vec![(tag_offset, val)]
1007                        }
1008                    } else {
1009                        // Niched or uninhabited variant that corresponds to no tag.
1010                        vec![]
1011                    };
1012
1013                    let field_offsets = variant_layout
1014                        .field_offsets
1015                        .iter()
1016                        .map(|o| OffsetExpr::new(o.bytes()))
1017                        .collect();
1018                    variant_layouts[variant_id] = Some(VariantLayout {
1019                        field_offsets,
1020                        inhabited: variant_inhabited,
1021                        tagger,
1022                    });
1023                }
1024
1025                let fallback = match tag_encoding {
1026                    r_abi::TagEncoding::Direct => Discriminator::Invalid,
1027                    // We follow what Minirust does:
1028                    // https://github.com/minirust/minirust/blob/master/tooling/minimize/src/enums.rs
1029                    r_abi::TagEncoding::Niche {
1030                        untagged_variant, ..
1031                    } => {
1032                        // Every value outside the valid range of the tag is invalid. The valid
1033                        // range is given as bits and may wrap around; we compare in `tag_ty`.
1034                        let valid = tag.valid_range(&self.t_ctx.tcx);
1035                        let start = tag_from_bits(valid.start);
1036                        let end = tag_from_bits(valid.end);
1037                        let (min, max) = match tag_ty {
1038                            IntegerTy::Signed(_) => (
1039                                tag_from_bits(tag_size.signed_int_min() as u128),
1040                                tag_from_bits(tag_size.signed_int_max() as u128),
1041                            ),
1042                            IntegerTy::Unsigned(_) => {
1043                                (tag_from_bits(0), tag_from_bits(tag_size.unsigned_int_max()))
1044                            }
1045                        };
1046
1047                        let after_end = tag_from_bits(valid.end.wrapping_add(1));
1048                        let before_start = tag_from_bits(valid.start.wrapping_sub(1));
1049                        if start <= end {
1050                            // The valid range is contiguous: the invalid values are on either side.
1051                            if end < max {
1052                                children.push((after_end..=max, Discriminator::Invalid));
1053                            }
1054                            if min < start {
1055                                children.push((min..=before_start, Discriminator::Invalid));
1056                            }
1057                        } else {
1058                            // The valid range wraps around: the invalid values are in the middle.
1059                            if after_end <= before_start {
1060                                children.push((after_end..=before_start, Discriminator::Invalid));
1061                            }
1062                        }
1063                        if variants[*untagged_variant].is_uninhabited() {
1064                            Discriminator::Invalid
1065                        } else {
1066                            Discriminator::Known(self.translate_variant_id(*untagged_variant))
1067                        }
1068                    }
1069                };
1070
1071                // The ranges are disjoint; sort them for readability.
1072                children.sort_by_key(|(range, _)| *range.start());
1073                let discriminator = Discriminator::Branch {
1074                    offset: tag_offset_expr,
1075                    int_ty: tag_ty,
1076                    fallback: Box::new(fallback),
1077                    children,
1078                };
1079
1080                Some(discriminator)
1081            }
1082            r_abi::Variants::Single { index } => {
1083                let variant_id = self.translate_variant_id(*index);
1084                match layout.fields() {
1085                    r_abi::FieldsShape::Arbitrary { .. } | r_abi::FieldsShape::Union(_) => {
1086                        let variant_inhabited = self
1087                            .translate_inhabited_predicate(span, rustc_variant_inhabited(*index))
1088                            .ok()?;
1089                        variant_layouts[variant_id] =
1090                            translate_variant_layout_data(&layout, variant_inhabited, vec![]);
1091                    }
1092                    r_abi::FieldsShape::Array { .. }
1093                        if matches!(ty.kind(), ty::Str)
1094                            && matches!(kind, TypeDeclKind::Struct(_)) =>
1095                    {
1096                        // Charon models `str` as a struct containing a single `[u8]` field.
1097                        variant_layouts[variant_id] = Some(VariantLayout {
1098                            field_offsets: [OffsetExpr::new(0)].into(),
1099                            inhabited: InhabitedPredicate::mk_true(),
1100                            tagger: vec![],
1101                        });
1102                    }
1103                    r_abi::FieldsShape::Primitive | r_abi::FieldsShape::Array { .. } => {}
1104                }
1105                Some(Discriminator::trivial(variant_id))
1106            }
1107            r_abi::Variants::Empty => None,
1108        };
1109
1110        let union_chunks = kind.is_union().then(|| {
1111            let mut markers = vec![false; ty_layout.size.bytes_usize()];
1112            mark_data_bytes(&layout_cx, ty_layout, &mut markers);
1113            let mut chunks = vec![];
1114            let mut offset = 0;
1115            for run in markers.chunk_by(|a, b| a == b) {
1116                if run[0] {
1117                    chunks.push((offset, run.len() as ByteCount));
1118                }
1119                offset += run.len() as ByteCount;
1120            }
1121            chunks
1122        });
1123
1124        Some(Layout {
1125            size,
1126            align,
1127            discriminator,
1128            inhabited,
1129            variant_layouts,
1130            union_chunks,
1131            repr,
1132        })
1133    }
1134
1135    /// Generate a naive layout for this type.
1136    pub fn generate_naive_layout(&self, span: Span, ty: &TypeDeclKind) -> Result<Layout, Error> {
1137        match ty {
1138            TypeDeclKind::Struct(fields) => {
1139                let mut size = 0;
1140                let mut align = 0;
1141                let ptr_size = self.translated.the_target_information().target_pointer_size;
1142                let field_offsets = fields.map_ref(|field| {
1143                    let offset = size;
1144                    let size_of_ty = match field.ty.kind() {
1145                        TyKind::Scalar(scalar_ty) => scalar_ty.target_size(ptr_size) as u64,
1146                        // This is a lie, the pointers could be fat...
1147                        TyKind::Ref(..) | TyKind::RawPtr(..) | TyKind::FnPtr(..) => ptr_size,
1148                        _ => panic!("Unsupported type for `generate_naive_layout`: {ty:?}"),
1149                    };
1150                    // For these types, align == size is good enough.
1151                    let align_of_ty = size_of_ty;
1152                    size += size_of_ty;
1153                    align = std::cmp::max(align, align_of_ty);
1154                    OffsetExpr::new(offset)
1155                });
1156
1157                Ok(Layout {
1158                    size: Size::new(size),
1159                    align: Size::new(align),
1160                    discriminator: None,
1161                    inhabited: InhabitedPredicate::mk_true(),
1162                    variant_layouts: IndexVec::from([Some(VariantLayout {
1163                        field_offsets,
1164                        tagger: vec![],
1165                        inhabited: InhabitedPredicate::mk_true(),
1166                    })]),
1167                    union_chunks: None,
1168                    repr: ReprOptions::default(),
1169                })
1170            }
1171            _ => raise_error!(
1172                self,
1173                span,
1174                "`generate_naive_layout` only supports structs at the moment"
1175            ),
1176        }
1177    }
1178
1179    /// Translate the body of a type declaration.
1180    ///
1181    /// Note that the type may be external, in which case we translate the body
1182    /// only if it is public (i.e., it is a public enumeration, or it is a
1183    /// struct with only public fields).
1184    pub(crate) fn translate_adt_def(
1185        &mut self,
1186        trans_id: TypeDeclId,
1187        def_span: Span,
1188        item_meta: &ItemMeta,
1189        def: &hax::FullDef<'tcx>,
1190    ) -> Result<TypeDeclKind, Error> {
1191        use crate::hax::AdtKind;
1192        let hax::FullDefKind::Adt(adt) = def.kind() else {
1193            unreachable!()
1194        };
1195
1196        if item_meta.opacity.is_opaque() {
1197            return Ok(TypeDeclKind::Opaque);
1198        }
1199
1200        let adt_kind = adt.adt_kind();
1201        if matches!(adt_kind, AdtKind::Tuple) && self.t_ctx.options.no_gen_tuple_structs {
1202            return Ok(TypeDeclKind::Opaque);
1203        }
1204
1205        // hax's synthetic ADTs have no variants; we must construct the fields ourselves
1206        let synthetic_fields = match adt_kind {
1207            AdtKind::Tuple => {
1208                let item = def.this();
1209                let args = self.translate_generic_args_without_trait_refs(def_span, item)?;
1210                Some(args.types.into_iter().collect_vec())
1211            }
1212            AdtKind::Str => {
1213                let u8_is_sized = self.translate_sized_proof(def_span, self.tcx.types.u8)?;
1214                Some(vec![Ty::mk_slice(Ty::mk_u8(), u8_is_sized)])
1215            }
1216            _ => None,
1217        };
1218        if let Some(tys) = synthetic_fields {
1219            let fields = tys
1220                .into_iter()
1221                .enumerate()
1222                .map(|(field_id, ty)| Field {
1223                    span: def_span,
1224                    attr_info: AttrInfo::dummy_public(),
1225                    name: format!("_{field_id}"),
1226                    is_positional: true,
1227                    ty,
1228                })
1229                .collect();
1230            return Ok(TypeDeclKind::Struct(fields));
1231        }
1232
1233        trace!("{}", trans_id);
1234
1235        // In case the type is external, check if we should consider the type as
1236        // transparent (i.e., extract its body). If it is an enumeration, then yes
1237        // (because the variants of public enumerations are public, together with their
1238        // fields). If it is a structure, we check if all the fields are public.
1239        let variants = adt.variants();
1240        let contents_are_public = match adt_kind {
1241            AdtKind::Enum => true,
1242            AdtKind::Struct | AdtKind::Union => {
1243                // Check the unique variant
1244                error_assert!(self, def_span, variants.len() == 1);
1245                variants[hax::VariantIdx::from(0usize)]
1246                    .fields
1247                    .iter()
1248                    .all(|f| matches!(f.vis, Visibility::Public))
1249            }
1250            // The rest are fake adt kinds that won't reach here.
1251            _ => unreachable!(),
1252        };
1253
1254        if item_meta
1255            .opacity
1256            .with_content_visibility(contents_are_public)
1257            .is_opaque()
1258        {
1259            return Ok(TypeDeclKind::Opaque);
1260        }
1261
1262        // The type is transparent: explore the variants
1263        let mut translated_variants: IndexVec<VariantId, Variant> = Default::default();
1264        for (i, var_def) in variants.iter().enumerate() {
1265            trace!("variant {i}: {var_def:?}");
1266
1267            let mut fields: IndexVec<FieldId, Field> = Default::default();
1268            for (j, field_def) in var_def.fields.iter().enumerate() {
1269                trace!("variant {i}: field {j}: {field_def:?}");
1270                let field_span = self.t_ctx.translate_span(&field_def.span);
1271                // Translate the field type
1272                let ty = self.translate_ty(field_span, &field_def.ty)?;
1273                let field_full_def = self.poly_hax_def(&field_def.did)?;
1274                let field_attrs = self.t_ctx.translate_attr_info(&field_full_def);
1275
1276                // Retrieve the field name.
1277                let is_positional = field_def.name.is_none();
1278                let field_name = field_def
1279                    .name
1280                    .map_or_else(|| format!("_{j}"), |name| name.to_string());
1281
1282                // Store the field
1283                let field = Field {
1284                    span: field_span,
1285                    attr_info: field_attrs,
1286                    name: field_name,
1287                    is_positional,
1288                    ty,
1289                };
1290                fields.push(field);
1291            }
1292
1293            let discriminant = self.translate_discriminant(def_span, &var_def.discr_val)?;
1294            let variant_span = self.t_ctx.translate_span(&var_def.span);
1295            let variant_name = var_def.name.to_string();
1296            let variant_full_def = self.poly_hax_def(&var_def.def_id)?;
1297
1298            let mut variant_attrs = self.t_ctx.translate_attr_info(&variant_full_def);
1299            // Propagate a `#[charon::variants_prefix(..)]` or `#[charon::variants_suffix(..)]` attribute to the variants.
1300            if variant_attrs.rename.is_none() {
1301                let prefix = item_meta
1302                    .attr_info
1303                    .attributes
1304                    .iter()
1305                    .filter_map(|a| a.as_variants_prefix())
1306                    .next()
1307                    .map(|attr| attr.as_str());
1308                let suffix = item_meta
1309                    .attr_info
1310                    .attributes
1311                    .iter()
1312                    .filter_map(|a| a.as_variants_suffix())
1313                    .next()
1314                    .map(|attr| attr.as_str());
1315                if prefix.is_some() || suffix.is_some() {
1316                    let prefix = prefix.unwrap_or_default();
1317                    let suffix = suffix.unwrap_or_default();
1318                    variant_attrs.rename = Some(format!("{prefix}{variant_name}{suffix}"));
1319                }
1320            }
1321
1322            translated_variants.push_with(|id| Variant {
1323                id,
1324                span: variant_span,
1325                attr_info: variant_attrs,
1326                name: variant_name,
1327                fields,
1328                discriminant,
1329            });
1330        }
1331
1332        // Register the type
1333        let type_def_kind: TypeDeclKind = match adt_kind {
1334            AdtKind::Struct => TypeDeclKind::Struct(translated_variants[0].fields.clone()),
1335            AdtKind::Enum => TypeDeclKind::Enum(translated_variants),
1336            AdtKind::Union => TypeDeclKind::Union(translated_variants[0].fields.clone()),
1337            // The rest are fake adt kinds that won't reach here.
1338            _ => unreachable!(),
1339        };
1340
1341        Ok(type_def_kind)
1342    }
1343
1344    fn translate_discriminant(
1345        &mut self,
1346        def_span: Span,
1347        discr: &hax::DiscriminantValue<'tcx>,
1348    ) -> Result<IntegerValue, Error> {
1349        let ty = self.translate_ty(def_span, &discr.ty)?;
1350        let scalar_ty = ty.kind().as_scalar().unwrap();
1351        match scalar_ty.as_integer() {
1352            Some(int_ty) => Ok(IntegerValue::from_bits(*int_ty, discr.val)),
1353            None => raise_error!(self, def_span, "unexpected discriminant type: {ty:?}",),
1354        }
1355    }
1356
1357    fn translate_inhabited_predicate(
1358        &mut self,
1359        span: Span,
1360        predicate: ty::inhabitedness::InhabitedPredicate<'tcx>,
1361    ) -> Result<InhabitedPredicate, Error> {
1362        use ty::inhabitedness::InhabitedPredicate as RustcPredicate;
1363        Ok(match predicate {
1364            RustcPredicate::True => InhabitedPredicateKind::True,
1365            RustcPredicate::False => InhabitedPredicateKind::False,
1366            RustcPredicate::ConstIsZero(value) => {
1367                InhabitedPredicateKind::ConstIsZero(self.translate_ty_constant_expr(span, &value)?)
1368            }
1369            // We only retain layout-relevant inhabitedness.
1370            RustcPredicate::NotInModule(_) => InhabitedPredicateKind::False,
1371            RustcPredicate::GenericType(ty) => {
1372                InhabitedPredicateKind::GenericType(self.translate_rustc_ty(span, &ty)?)
1373            }
1374            RustcPredicate::OpaqueType(key) => {
1375                // Reveal the opaque type.
1376                let opaque_ty = self
1377                    .tcx
1378                    .type_of(key.def_id)
1379                    .instantiate(self.tcx, key.args)
1380                    .skip_norm_wip();
1381                return self
1382                    .translate_inhabited_predicate(span, opaque_ty.inhabited_predicate(self.tcx));
1383            }
1384            RustcPredicate::And(&[left, right]) => InhabitedPredicateKind::And(vec![
1385                self.translate_inhabited_predicate(span, left)?,
1386                self.translate_inhabited_predicate(span, right)?,
1387            ]),
1388            RustcPredicate::Or(&[left, right]) => InhabitedPredicateKind::Or(vec![
1389                self.translate_inhabited_predicate(span, left)?,
1390                self.translate_inhabited_predicate(span, right)?,
1391            ]),
1392        }
1393        .into_pred())
1394    }
1395
1396    pub fn translate_repr_options(&mut self, hax_repr_options: &hax::ReprOptions) -> ReprOptions {
1397        let repr_algo = if hax_repr_options.flags.is_simd {
1398            ReprAlgorithm::Simd
1399        } else if hax_repr_options.flags.is_c {
1400            ReprAlgorithm::C
1401        } else {
1402            ReprAlgorithm::Rust
1403        };
1404
1405        let align_mod = if let Some(align) = &hax_repr_options.align {
1406            Some(AlignmentModifier::Align(align.bytes()))
1407        } else if let Some(pack) = &hax_repr_options.pack {
1408            Some(AlignmentModifier::Pack(pack.bytes()))
1409        } else {
1410            None
1411        };
1412
1413        let explicit_discr_type =
1414            hax_repr_options
1415                .int_specified
1416                .then(|| match hax_repr_options.typ.kind() {
1417                    hax::TyKind::Int(ty) => IntegerTy::Signed(Self::translate_hax_int_ty(ty)),
1418                    hax::TyKind::Uint(ty) => IntegerTy::Unsigned(Self::translate_hax_uint_ty(ty)),
1419                    ty => unreachable!("explicit enum discriminant type is not an integer: {ty:?}"),
1420                });
1421
1422        ReprOptions {
1423            transparent: hax_repr_options.flags.is_transparent,
1424            explicit_discr_type,
1425            repr_algo,
1426            align_modif: align_mod,
1427        }
1428    }
1429}
charon_driver/translate/translate_types.rs

charon_driver/translate/
translate_types.rs
