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    pub(crate) fn translate_sized_proof(
13        &mut self,
14        span: Span,
15        ty: ty::Ty<'tcx>,
16    ) -> Result<Option<TraitRef>, Error> {
17        if self.options.hide_marker_traits {
18            return Ok(None);
19        }
20        let proof = hax::solve_sized(&self.hax_state, ty);
21        self.translate_trait_proof(span, &proof).map(Some)
22    }
23
24    /// Translate an erased region. If we're inside a body, this will return a fresh body region
25    /// instead.
26    pub(crate) fn translate_erased_region(&mut self) -> Region {
27        if let Some(v) = &mut self.lifetime_freshener {
28            Region::Body(v.push(()))
29        } else {
30            Region::Erased
31        }
32    }
33
34    /// Erase a region binder by supplying erased lifetimes (or fresh body lifetimes) for all its
35    /// arguments.
36    pub(crate) fn erase_region_binder<T: TyVisitable>(&mut self, b: RegionBinder<T>) -> T {
37        let regions = b
38            .regions
39            .map_ref_indexed(|_, _| self.translate_erased_region());
40        b.apply(regions)
41    }
42
43    // Translate a region
44    pub(crate) fn translate_region(
45        &mut self,
46        span: Span,
47        region: &hax::Region,
48    ) -> Result<Region, Error> {
49        use crate::hax::RegionKind::*;
50        match &region.kind {
51            ReErased => Ok(self.translate_erased_region()),
52            ReStatic => Ok(Region::Static),
53            ReBound(hax::BoundVarIndexKind::Bound(id), br) => {
54                Ok(match self.lookup_bound_region(span, *id, br.var) {
55                    Ok(var) => Region::Var(var),
56                    Err(_) => Region::Erased,
57                })
58            }
59            ReEarlyParam(region) => Ok(match self.lookup_early_region(span, region) {
60                Ok(var) => Region::Var(var),
61                Err(_) => Region::Erased,
62            }),
63            ReLateParam(region) => Ok(Region::Var(self.lookup_late_param_region(span, region)?)),
64            ReVar(..) | RePlaceholder(..) => {
65                // Shouldn't exist outside of type inference.
66                raise_error!(
67                    self,
68                    span,
69                    "Should not exist outside of type inference: {region:?}"
70                )
71            }
72            ReBound(..) | ReError(..) => {
73                raise_error!(self, span, "Unexpected region kind: {region:?}")
74            }
75        }
76    }
77
78    pub(crate) fn translate_hax_int_ty(int_ty: &hax::IntTy) -> IntTy {
79        match int_ty {
80            hax::IntTy::Isize => IntTy::Isize,
81            hax::IntTy::I8 => IntTy::I8,
82            hax::IntTy::I16 => IntTy::I16,
83            hax::IntTy::I32 => IntTy::I32,
84            hax::IntTy::I64 => IntTy::I64,
85            hax::IntTy::I128 => IntTy::I128,
86        }
87    }
88
89    pub(crate) fn translate_hax_uint_ty(uint_ty: &hax::UintTy) -> UIntTy {
90        use crate::hax::UintTy;
91        match uint_ty {
92            UintTy::Usize => UIntTy::Usize,
93            UintTy::U8 => UIntTy::U8,
94            UintTy::U16 => UIntTy::U16,
95            UintTy::U32 => UIntTy::U32,
96            UintTy::U64 => UIntTy::U64,
97            UintTy::U128 => UIntTy::U128,
98        }
99    }
100
101    /// Translate a Ty.
102    ///
103    /// Typically used in this module to translate the fields of a structure/
104    /// enumeration definition, or later to translate the type of a variable.
105    ///
106    /// Note that we take as parameter a function to translate regions, because
107    /// regions can be translated in several manners (non-erased region or erased
108    /// regions), in which case the return type is different.
109    #[tracing::instrument(skip(self, span))]
110    pub(crate) fn translate_ty(&mut self, span: Span, hax_ty: &hax::Ty) -> Result<Ty, Error> {
111        let mut ty = if let Some(ty) = self
112            .innermost_binder()
113            .type_trans_cache
114            .get(hax_ty)
115            .cloned()
116        {
117            ty
118        } else {
119            let ty = self
120                .translate_ty_inner(span, hax_ty)
121                .unwrap_or_else(|e| TyKind::Error(e.msg).into_ty());
122            self.innermost_binder_mut()
123                .type_trans_cache
124                .insert(hax_ty.clone(), ty.clone());
125            ty
126        };
127        if let Some(v) = &mut self.lifetime_freshener {
128            // We might be reusing a value from cache: we must refresh the erased & body regions.
129            ty = ty.replace_erased_regions(|| Region::Body(v.push(())));
130        }
131        Ok(ty)
132    }
133
134    fn translate_ty_inner(&mut self, span: Span, ty: &hax::Ty) -> Result<Ty, Error> {
135        trace!("{:?}", ty);
136        let kind = match ty.kind() {
137            hax::TyKind::Bool => TyKind::Scalar(ScalarTy::Bool),
138            hax::TyKind::Char => TyKind::Scalar(ScalarTy::Char),
139            hax::TyKind::Int(int_ty) => TyKind::Scalar(ScalarTy::Integer(IntegerTy::Signed(
140                Self::translate_hax_int_ty(int_ty),
141            ))),
142            hax::TyKind::Uint(uint_ty) => TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(
143                Self::translate_hax_uint_ty(uint_ty),
144            ))),
145            hax::TyKind::Float(float_ty) => TyKind::Scalar(ScalarTy::Float(match float_ty {
146                hax::FloatTy::F16 => FloatTy::F16,
147                hax::FloatTy::F32 => FloatTy::F32,
148                hax::FloatTy::F64 => FloatTy::F64,
149                hax::FloatTy::F128 => FloatTy::F128,
150            })),
151            hax::TyKind::Never => TyKind::Never,
152
153            hax::TyKind::Alias(alias) => match &alias.kind {
154                hax::AliasKind::Projection(item) => {
155                    let trait_ref = self.translate_trait_proof(
156                        span,
157                        item.in_trait
158                            .as_ref()
159                            .expect("projection without a trait_ref?"),
160                    )?;
161                    let assoc_type_id =
162                        self.translate_assoc_type_id(trait_ref.trait_id(), &item.def_id)?;
163                    let generics =
164                        self.translate_generic_args(span, &item.generic_args, &item.trait_proofs)?;
165                    TyKind::TraitType(trait_ref, assoc_type_id, generics)
166                }
167                hax::AliasKind::Opaque { hidden_ty, .. } => {
168                    return self.translate_ty(span, hidden_ty);
169                }
170                _ => {
171                    raise_error!(self, span, "Unsupported alias type: {:?}", alias.kind)
172                }
173            },
174
175            hax::TyKind::Adt(item) => {
176                let tref = self.translate_type_decl_ref(span, item)?;
177                TyKind::Adt(tref)
178            }
179            hax::TyKind::Str(item_ref) => {
180                let tref = self.translate_type_decl_ref(span, item_ref)?;
181                TyKind::Adt(tref)
182            }
183            hax::TyKind::Array(item_ref) => {
184                // `Sized` is the first predicate if we're not hiding marker traits.
185                let item_ty_is_sized = if self.options.hide_marker_traits {
186                    None
187                } else {
188                    Some(self.translate_trait_proof(span, &item_ref.trait_proofs[0])?)
189                };
190                let mut args = self.translate_generic_args(span, &item_ref.generic_args, &[])?;
191                assert!(args.types.len() == 1 && args.const_generics.len() == 1);
192                TyKind::Array(
193                    args.types.pop().unwrap(),
194                    args.const_generics.pop().unwrap(),
195                    item_ty_is_sized,
196                )
197            }
198            hax::TyKind::Pat(ty, pat) => {
199                let ty = self.translate_ty(span, ty)?;
200                let pat = self.translate_pattern(span, pat)?;
201                TyKind::Pattern(ty, pat)
202            }
203            hax::TyKind::Slice(item_ref) => {
204                // `Sized` is the first predicate if we're not hiding marker traits.
205                let item_ty_is_sized = if self.options.hide_marker_traits {
206                    None
207                } else {
208                    Some(self.translate_trait_proof(span, &item_ref.trait_proofs[0])?)
209                };
210                let mut args = self.translate_generic_args(span, &item_ref.generic_args, &[])?;
211                assert!(args.types.len() == 1);
212                TyKind::Slice(args.types.pop().unwrap(), item_ty_is_sized)
213            }
214            hax::TyKind::Tuple(item_ref) => {
215                let tref = self.translate_type_decl_ref(span, item_ref)?;
216                TyKind::Adt(tref)
217            }
218            hax::TyKind::Ref(region, ty, mutability) => {
219                trace!("Ref");
220
221                let region = self.translate_region(span, region)?;
222                let ty = self.translate_ty(span, ty)?;
223                let kind = if mutability.is_mut() {
224                    RefKind::Mut
225                } else {
226                    RefKind::Shared
227                };
228                TyKind::Ref(region, ty, kind)
229            }
230            hax::TyKind::RawPtr(ty, mutbl) => {
231                trace!("RawPtr: {:?}", (ty, mutbl));
232                let ty = self.translate_ty(span, ty)?;
233                let kind = if mutbl.is_mut() {
234                    RefKind::Mut
235                } else {
236                    RefKind::Shared
237                };
238                TyKind::RawPtr(ty, kind)
239            }
240
241            hax::TyKind::Param(param) => {
242                // A type parameter, for example `T` in `fn f<T>(x : T) {}`.
243                // Note that this type parameter may actually have been
244                // instantiated (in our environment, we may map it to another
245                // type): we just have to look it up.
246                // Note that if we are using this function to translate a field
247                // type in a type definition, it should actually map to a type
248                // parameter.
249                match self.lookup_type_var(span, param) {
250                    Ok(var) => TyKind::TypeVar(var),
251                    Err(err) => TyKind::Error(err.msg),
252                }
253            }
254
255            hax::TyKind::Foreign(item) => {
256                let tref = self.translate_type_decl_ref(span, item)?;
257                TyKind::Adt(tref)
258            }
259
260            hax::TyKind::Arrow(sig) => {
261                trace!("Arrow");
262                trace!("bound vars: {:?}", sig.bound_vars);
263                let sig = self.translate_poly_fun_sig(span, sig)?;
264                TyKind::FnPtr(sig)
265            }
266            hax::TyKind::FnDef { item, .. } => {
267                let fnref = self.translate_bound_fn_ptr(span, item, TransItemSourceKind::Fun)?;
268                TyKind::FnDef(fnref)
269            }
270            hax::TyKind::Closure(args) => {
271                let tref = self.translate_closure_type_ref(span, args)?;
272                TyKind::Adt(tref)
273            }
274
275            hax::TyKind::Dynamic(dyn_binder, region) => {
276                // self.check_no_monomorphize(span)?;
277                // Translate the region outside the binder.
278                let region = self.translate_region(span, region)?;
279
280                let binder = self.translate_dyn_binder(span, dyn_binder, |ctx, ty, ()| {
281                    let region = region.move_under_binder();
282                    ctx.innermost_binder_mut()
283                        .params
284                        .types_outlive
285                        .push(RegionBinder::empty(OutlivesPred(ty.clone(), region)));
286                    Ok(ty)
287                })?;
288
289                if let hax::ClauseKind::Trait(trait_predicate) = dyn_binder.predicates.predicates[0]
290                    .clause
291                    .kind
292                    .hax_skip_binder_ref()
293                {
294                    // TODO(dyn): for now, we consider traits with associated types to not be dyn
295                    // compatible because we don't know how to handle them; for these we skip
296                    // translating the vtable.
297                    if self.trait_is_dyn_compatible(&trait_predicate.trait_ref.def_id)? {
298                        // Ensure the vtable type is translated. The first predicate is the one that
299                        // can have methods, i.e. a vtable.
300                        let _: TypeDeclId = self.register_item(
301                            span,
302                            &trait_predicate.trait_ref,
303                            TransItemSourceKind::VTable,
304                        );
305                    }
306                }
307                TyKind::DynTrait(DynPredicate { binder })
308            }
309
310            hax::TyKind::Infer(_) => {
311                raise_error!(self, span, "Unsupported type: infer type")
312            }
313            hax::TyKind::Coroutine(..) => {
314                raise_error!(self, span, "Coroutine types are not supported yet")
315            }
316            hax::TyKind::Bound(_, _) => {
317                raise_error!(self, span, "Unexpected type kind: bound")
318            }
319            hax::TyKind::Placeholder(_) => {
320                raise_error!(self, span, "Unsupported type: placeholder")
321            }
322
323            hax::TyKind::Error => {
324                raise_error!(self, span, "Type checking error")
325            }
326            hax::TyKind::Todo(s) => {
327                raise_error!(self, span, "Unsupported type: {:?}", s)
328            }
329        };
330        Ok(kind.into_ty())
331    }
332
333    pub fn translate_pattern(
334        &mut self,
335        span: Span,
336        pat: &hax::Pattern,
337    ) -> Result<TypePattern, Error> {
338        Ok(match pat {
339            hax::Pattern::Range { start, end } => TypePattern::Range(
340                self.translate_constant_expr(span, start)?,
341                self.translate_constant_expr(span, end)?,
342            ),
343            hax::Pattern::Or(patterns) => TypePattern::OrPattern(
344                patterns
345                    .iter()
346                    .map(|pat| self.translate_pattern(span, pat))
347                    .try_collect()?,
348            ),
349            hax::Pattern::NotNull => TypePattern::NotNull,
350        })
351    }
352
353    pub(crate) fn translate_rustc_ty(
354        &mut self,
355        span: Span,
356        ty: &ty::Ty<'tcx>,
357    ) -> Result<Ty, Error> {
358        let ty = self.t_ctx.catch_sinto(&self.hax_state, span, ty)?;
359        self.translate_ty(span, &ty)
360    }
361
362    pub fn translate_poly_fun_sig(
363        &mut self,
364        span: Span,
365        sig: &hax::Binder<hax::TyFnSig>,
366    ) -> Result<RegionBinder<FunSig>, Error> {
367        self.translate_region_binder(span, sig, |ctx, sig| ctx.translate_fun_sig(span, sig))
368    }
369    pub fn translate_fun_sig(&mut self, span: Span, sig: &hax::TyFnSig) -> Result<FunSig, Error> {
370        let inputs = sig
371            .inputs
372            .iter()
373            .map(|x| self.translate_ty(span, x))
374            .try_collect()?;
375        let output = self.translate_ty(span, &sig.output)?;
376        Ok(FunSig {
377            is_unsafe: sig.safety == hax::Safety::Unsafe,
378            abi: Self::translate_abi(&sig.abi),
379            is_variadic: sig.c_variadic,
380            inputs,
381            output,
382        })
383    }
384
385    pub fn translate_abi(abi: &hax::ExternAbi) -> Abi {
386        match abi {
387            hax::ExternAbi::Rust => Abi::Rust,
388            hax::ExternAbi::C { unwind: false } => Abi::C,
389            _ => Abi::Other(abi.as_str().into()),
390        }
391    }
392
393    /// Translate generic args. Don't call directly; use `translate_xxx_ref` as much as possible.
394    pub fn translate_generic_args(
395        &mut self,
396        span: Span,
397        substs: &[hax::GenericArg],
398        trait_refs: &[hax::TraitProof],
399    ) -> Result<GenericArgs, Error> {
400        use crate::hax::GenericArg::*;
401        trace!("{:?}", substs);
402
403        let mut regions = IndexVec::new();
404        let mut types = IndexVec::new();
405        let mut const_generics = IndexVec::new();
406        for param in substs {
407            match param {
408                Type(param_ty) => {
409                    types.push(self.translate_ty(span, param_ty)?);
410                }
411                Lifetime(region) => {
412                    regions.push(self.translate_region(span, region)?);
413                }
414                Const(c) => {
415                    const_generics.push(self.translate_constant_expr(span, c)?);
416                }
417            }
418        }
419        let trait_refs = self.translate_trait_proofs(span, trait_refs)?;
420
421        Ok(GenericArgs {
422            regions,
423            types,
424            const_generics,
425            trait_refs,
426        })
427    }
428
429    /// Whether Rust treats this type specially, i.e. whether it is a tuple, `str` or `Box`.
430    pub(crate) fn recognize_builtin_adt(&mut self, item: &hax::ItemRef) -> Option<BuiltinAdt> {
431        item.def_id
432            .as_synthetic(self.hax_state())
433            .and_then(|synthetic| match synthetic {
434                hax::SyntheticItem::Tuple(_) => Some(BuiltinAdt::Tuple),
435                hax::SyntheticItem::Str => Some(BuiltinAdt::Str),
436                hax::SyntheticItem::Array | hax::SyntheticItem::Slice => None,
437            })
438            .or_else(|| {
439                (self.hax_def(item).ok()?.lang_item? == sym::owned_box).then_some(BuiltinAdt::Box)
440            })
441    }
442
443    /// Translate a Dynamically Sized Type metadata kind.
444    ///
445    /// Returns `None` if the type is generic, or if it is not a DST.
446    pub fn translate_ptr_metadata(
447        &mut self,
448        span: Span,
449        item: &hax::ItemRef,
450    ) -> Result<PtrMetadata, Error> {
451        // prepare the call to the method
452        use rustc_middle::ty;
453        let tcx = self.t_ctx.tcx;
454        let hax_state = &self.hax_state;
455        let ty_env = hax_state.typing_env();
456        let ty = item
457            .def_id
458            .type_of(hax_state)
459            .instantiate(tcx, item.rustc_args(hax_state));
460        let ty = hax::normalize(tcx, ty_env, ty);
461
462        // Get the tail type, which determines the metadata of `ty`.
463        let tail_ty = tcx.struct_tail_raw(
464            ty,
465            &rustc_middle::traits::ObligationCause::dummy(),
466            |ty| hax::normalize(tcx, ty_env, ty),
467            || {},
468        );
469        let hax_ty: hax::Ty = self.t_ctx.catch_sinto(hax_state, span, &tail_ty)?;
470
471        // If we're hiding `Sized`, let's consider everything to be sized.
472        let everything_is_sized = self.t_ctx.options.hide_marker_traits;
473        let ret = match tail_ty.kind() {
474            _ if everything_is_sized || tail_ty.is_sized(tcx, ty_env) => PtrMetadata::None,
475            ty::Str | ty::Slice(..) => PtrMetadata::Length,
476            ty::Dynamic(..) => match hax_ty.kind() {
477                hax::TyKind::Dynamic(dyn_binder, _) => {
478                    let vtable = self.translate_dyn_binder(span, dyn_binder, |ctx, _, _| {
479                        ctx.translate_region_binder(
480                            span,
481                            &dyn_binder.predicates.predicates[0].clause.kind,
482                            |ctx, kind: &hax::ClauseKind| {
483                                let hax::ClauseKind::Trait(trait_predicate) = kind else {
484                                    unreachable!()
485                                };
486                                ctx.translate_vtable_struct_ref(span, &trait_predicate.trait_ref)
487                            },
488                        )
489                    })?;
490                    let vtable = vtable
491                        .skip_binder
492                        .try_substitute(&GenericArgs::empty())
493                        .expect("vtable struct should not depend on self type");
494                    let vtable = self.erase_region_binder(vtable);
495                    PtrMetadata::VTable(vtable)
496                }
497                _ => unreachable!("Unexpected hax type {hax_ty:?} for dynamic type: {ty:?}"),
498            },
499            ty::Param(..) => PtrMetadata::InheritFrom(self.translate_ty(span, &hax_ty)?),
500            ty::Placeholder(..) | ty::Infer(..) | ty::Bound(..) => {
501                panic!(
502                    "We should never encounter a placeholder, infer, or bound type from ptr_metadata translation. Got: {tail_ty:?}"
503                )
504            }
505            _ => PtrMetadata::None,
506        };
507
508        Ok(ret)
509    }
510
511    /// Translate a type layout.
512    ///
513    /// Translates the layout as queried from rustc into the more restricted [`Layout`].
514    #[tracing::instrument(skip(self))]
515    pub fn translate_layout(
516        &mut self,
517        span: Span,
518        def: &hax::FullDef<'tcx>,
519        kind: &TypeDeclKind,
520    ) -> Option<Layout> {
521        let item = def.this();
522        use rustc_abi as r_abi;
523
524        fn translate_variant_layout_data(
525            layout_data: &r_abi::LayoutData<r_abi::FieldIdx, r_abi::VariantIdx>,
526            inhabited: InhabitedPredicate,
527            tagger: Vec<(ByteCount, IntegerValue)>,
528        ) -> Option<VariantLayout> {
529            let field_offsets = match &layout_data.fields {
530                r_abi::FieldsShape::Arbitrary { offsets, .. } => {
531                    offsets.iter().map(|o| OffsetExpr::new(o.bytes())).collect()
532                }
533                r_abi::FieldsShape::Union(n) => (0..n.get()).map(|_| OffsetExpr::new(0)).collect(),
534                r_abi::FieldsShape::Primitive => IndexVec::default(),
535                r_abi::FieldsShape::Array { .. } => panic!("Unexpected layout shape"),
536            };
537            Some(VariantLayout {
538                field_offsets,
539                inhabited,
540                tagger,
541            })
542        }
543
544        fn translate_primitive_int(int_ty: r_abi::Integer, signed: bool) -> IntegerTy {
545            if signed {
546                IntegerTy::Signed(match int_ty {
547                    r_abi::Integer::I8 => IntTy::I8,
548                    r_abi::Integer::I16 => IntTy::I16,
549                    r_abi::Integer::I32 => IntTy::I32,
550                    r_abi::Integer::I64 => IntTy::I64,
551                    r_abi::Integer::I128 => IntTy::I128,
552                })
553            } else {
554                IntegerTy::Unsigned(match int_ty {
555                    r_abi::Integer::I8 => UIntTy::U8,
556                    r_abi::Integer::I16 => UIntTy::U16,
557                    r_abi::Integer::I32 => UIntTy::U32,
558                    r_abi::Integer::I64 => UIntTy::U64,
559                    r_abi::Integer::I128 => UIntTy::U128,
560                })
561            }
562        }
563
564        /// Returns expressions that compute the layout (size, align) chosen by rustc. For sized
565        /// types, that's plain integers; for unsized types, we build expressions that compute the
566        /// right value based on pointer metadata values. This mirrors rustc's
567        /// `size_and_align_of_dst` computation:
568        /// <https://github.com/rust-lang/rust/blob/3fbb92e14159dd8b9bdb81e065883d1132e5abb7/compiler/rustc_codegen_ssa/src/size_of_val.rs#L100-L182>.
569        fn chosen_size_and_align<'tcx>(
570            cx: &ty::layout::LayoutCx<'tcx>,
571            layout: ty::layout::TyAndLayout<'tcx>,
572        ) -> Option<(SizeExpr, SizeExpr)> {
573            let constant = |value: u64| SizeExprKind::from_usize(u128::from(value)).into_expr();
574
575            if layout.is_sized() {
576                return Some((
577                    constant(layout.size.bytes()),
578                    constant(layout.align.abi.bytes()),
579                ));
580            }
581
582            match layout.ty.kind() {
583                ty::Dynamic(..) => Some((
584                    SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
585                    SizeExprKind::FromMetadata(MetadataValue::DynAlign).into_expr(),
586                )),
587                ty::Slice(..) | ty::Str => {
588                    let unit = layout.field(cx, 0);
589                    Some((
590                        SizeExprKind::Scale(
591                            SizeExprKind::FromMetadata(MetadataValue::SliceLength).into_expr(),
592                            ConstantExpr::mk_usize(u128::from(unit.size.bytes())),
593                        )
594                        .into_expr(),
595                        constant(unit.align.abi.bytes()),
596                    ))
597                }
598                ty::Adt(..) | ty::Tuple(..) => {
599                    let tail_idx = layout.fields.count() - 1;
600                    let tail_offset = constant(layout.fields.offset(tail_idx).bytes());
601                    let sized_align = constant(layout.align.abi.bytes());
602                    let tail_layout = layout.field(cx, tail_idx);
603                    let (tail_size, mut tail_align) = chosen_size_and_align(cx, tail_layout)?;
604
605                    if let ty::Adt(def, _) = layout.ty.kind()
606                        && let Some(pack) = def.repr().pack
607                    {
608                        tail_align =
609                            SizeExprKind::Min(vec![tail_align, constant(pack.bytes())]).into_expr();
610                    }
611
612                    let full_align = SizeExprKind::Max(vec![sized_align, tail_align]).into_expr();
613                    let full_size = SizeExprKind::AlignTo {
614                        base: SizeExprKind::Plus(tail_offset, tail_size).into_expr(),
615                        target_align: full_align.clone(),
616                    }
617                    .into_expr();
618                    Some((full_size, full_align))
619                }
620                ty::Foreign(..) => None,
621                _ => None,
622            }
623        }
624
625        let tcx = self.t_ctx.tcx;
626        let hax_state = self.hax_state_with_id();
627        assert_eq!(hax_state.owner(), item.def_id);
628        let ty_env = hax_state.typing_env();
629        let ty = item
630            .def_id
631            .type_of(hax_state)
632            .instantiate(tcx, item.rustc_args(hax_state));
633        let ty = hax::normalize(tcx, ty_env, ty);
634        let pseudo_input = ty_env.as_query_input(ty);
635        let ptr_size = self.translated.the_target_information().target_pointer_size;
636
637        let repr = match &def.kind {
638            hax::FullDefKind::Adt { repr: hax_repr, .. } => self.translate_repr_options(hax_repr),
639            _ => ReprOptions::default(),
640        };
641        let ty_layout = match tcx.layout_of(pseudo_input) {
642            Ok(layout) => layout,
643            Err(_) => return Layout::for_type(&self.translated, kind, repr),
644        };
645        let rustc_variant_inhabited = |id| match ty.kind() {
646            ty::Adt(adt, args) if adt.is_enum() => adt
647                .variant(id)
648                .inhabited_predicate(tcx, *adt)
649                .instantiate(tcx, args),
650            _ => ty.inhabited_predicate(tcx),
651        };
652        let inhabited = self
653            .translate_inhabited_predicate(span, ty.inhabited_predicate(tcx))
654            .ok()?;
655        let layout_cx = ty::layout::LayoutCx::new(tcx, ty_env);
656        let (size, align) = chosen_size_and_align(&layout_cx, ty_layout)?;
657        let size = Size::from_expr(size.normalize(Some(&self.translated), None, false));
658        let align = Size::from_expr(align.normalize(Some(&self.translated), None, false));
659        let layout = ty_layout.layout;
660
661        let num_variants = match ty.variant_range(self.t_ctx.tcx) {
662            Some(range) => range.end.index(),
663            None => match layout.fields() {
664                r_abi::FieldsShape::Arbitrary { .. } | r_abi::FieldsShape::Union(_) => 1,
665                r_abi::FieldsShape::Primitive | r_abi::FieldsShape::Array { .. } => 0,
666            },
667        };
668        let mut variant_layouts: IndexVec<VariantId, Option<VariantLayout>> =
669            (0..num_variants).map(|_| None).collect();
670        // Build the discriminator tree and variant layouts.
671        let discriminator = match layout.variants() {
672            r_abi::Variants::Multiple {
673                tag,
674                tag_encoding,
675                tag_field,
676                variants,
677                ..
678            } => {
679                // The tag_field is the index into the `offsets` vector.
680                let r_abi::FieldsShape::Arbitrary { offsets, .. } = layout.fields() else {
681                    unreachable!()
682                };
683                let tag_offset = offsets
684                    .get(*tag_field)
685                    .map(|s| r_abi::Size::bytes(*s))
686                    .expect("No tag field offset for enum?");
687                let tag_offset_expr = OffsetExpr::new(tag_offset);
688
689                let tag_ty = match tag.primitive() {
690                    r_abi::Primitive::Int(int_ty, signed) => {
691                        translate_primitive_int(int_ty, signed)
692                    }
693                    r_abi::Primitive::Pointer(_) => IntegerTy::Signed(IntTy::Isize),
694                    r_abi::Primitive::Float(_) => unreachable!(),
695                };
696                let tag_size = r_abi::Size::from_bytes(tag_ty.target_size(ptr_size));
697                // Reinterpret raw tag bits in `tag_ty`, sign-extending if needed.
698                let tag_from_bits =
699                    |bits: u128| IntegerValue::from_bits(tag_ty, tag_size.truncate(bits));
700
701                struct VariantTagInfo {
702                    /// The value of the tag for this variant, even if this is the untagged variant
703                    /// of a niched enum. `None` if we can't compute it.
704                    value: Option<IntegerValue>,
705                    /// Whether the variant is inhabited or not.
706                    uninhabited: bool,
707                    /// Whether this is the niched (untagged) variant of a niched enum.
708                    niched: bool,
709                }
710                let taginfo_for_variant = |id: rustc_abi::VariantIdx| {
711                    let uninhabited = variants[id].is_uninhabited();
712                    match tag_encoding {
713                        r_abi::TagEncoding::Direct => {
714                            let value = if uninhabited {
715                                None
716                            } else {
717                                let tag = tcx
718                                    .tag_for_variant(ty_env.as_query_input((ty, id)))
719                                    .unwrap();
720                                Some(tag_from_bits(tag.to_bits(tag_size)))
721                            };
722                            VariantTagInfo {
723                                value,
724                                uninhabited,
725                                niched: false,
726                            }
727                        }
728                        r_abi::TagEncoding::Niche {
729                            untagged_variant,
730                            niche_variants,
731                            niche_start,
732                        } => {
733                            let value = niche_variants.contains(&id).then(|| {
734                                let relative = (id.index() - niche_variants.start.index()) as u128;
735                                tag_from_bits(niche_start.wrapping_add(relative))
736                            });
737                            VariantTagInfo {
738                                value,
739                                uninhabited,
740                                niched: id == *untagged_variant,
741                            }
742                        }
743                    }
744                };
745
746                // Compute per-variant tag values and build tagger + discriminator children.
747                let mut children = Vec::new();
748
749                for (id, variant_layout) in variants.iter_enumerated() {
750                    let variant_id = self.translate_variant_id(id);
751                    let taginfo = taginfo_for_variant(id);
752                    let variant_inhabited = self
753                        .translate_inhabited_predicate(span, rustc_variant_inhabited(id))
754                        .ok()?;
755                    let tagger = if let Some(val) = taginfo.value {
756                        if taginfo.niched || taginfo.uninhabited {
757                            // If we could compute a tag for this variant, encountering it is UB.
758                            children.push((val..=val, Discriminator::Invalid));
759                            vec![]
760                        } else {
761                            children.push((val..=val, Discriminator::Known(variant_id)));
762                            vec![(tag_offset, val)]
763                        }
764                    } else {
765                        // Niched or uninhabited variant that corresponds to no tag.
766                        vec![]
767                    };
768
769                    let field_offsets = variant_layout
770                        .field_offsets
771                        .iter()
772                        .map(|o| OffsetExpr::new(o.bytes()))
773                        .collect();
774                    variant_layouts[variant_id] = Some(VariantLayout {
775                        field_offsets,
776                        inhabited: variant_inhabited,
777                        tagger,
778                    });
779                }
780
781                let fallback = match tag_encoding {
782                    r_abi::TagEncoding::Direct => Discriminator::Invalid,
783                    // We follow what Minirust does:
784                    // https://github.com/minirust/minirust/blob/master/tooling/minimize/src/enums.rs
785                    r_abi::TagEncoding::Niche {
786                        untagged_variant, ..
787                    } => {
788                        // Every value outside the valid range of the tag is invalid. The valid
789                        // range is given as bits and may wrap around; we compare in `tag_ty`.
790                        let valid = tag.valid_range(&self.t_ctx.tcx);
791                        let start = tag_from_bits(valid.start);
792                        let end = tag_from_bits(valid.end);
793                        let (min, max) = match tag_ty {
794                            IntegerTy::Signed(_) => (
795                                tag_from_bits(tag_size.signed_int_min() as u128),
796                                tag_from_bits(tag_size.signed_int_max() as u128),
797                            ),
798                            IntegerTy::Unsigned(_) => {
799                                (tag_from_bits(0), tag_from_bits(tag_size.unsigned_int_max()))
800                            }
801                        };
802
803                        let after_end = tag_from_bits(valid.end.wrapping_add(1));
804                        let before_start = tag_from_bits(valid.start.wrapping_sub(1));
805                        if start <= end {
806                            // The valid range is contiguous: the invalid values are on either side.
807                            if end < max {
808                                children.push((after_end..=max, Discriminator::Invalid));
809                            }
810                            if min < start {
811                                children.push((min..=before_start, Discriminator::Invalid));
812                            }
813                        } else {
814                            // The valid range wraps around: the invalid values are in the middle.
815                            if after_end <= before_start {
816                                children.push((after_end..=before_start, Discriminator::Invalid));
817                            }
818                        }
819                        if variants[*untagged_variant].is_uninhabited() {
820                            Discriminator::Invalid
821                        } else {
822                            Discriminator::Known(self.translate_variant_id(*untagged_variant))
823                        }
824                    }
825                };
826
827                // The ranges are disjoint; sort them for readability.
828                children.sort_by_key(|(range, _)| *range.start());
829                let discriminator = Discriminator::Branch {
830                    offset: tag_offset_expr,
831                    int_ty: tag_ty,
832                    fallback: Box::new(fallback),
833                    children,
834                };
835
836                Some(discriminator)
837            }
838            r_abi::Variants::Single { index } => {
839                let variant_id = self.translate_variant_id(*index);
840                match layout.fields() {
841                    r_abi::FieldsShape::Arbitrary { .. } | r_abi::FieldsShape::Union(_) => {
842                        let variant_inhabited = self
843                            .translate_inhabited_predicate(span, rustc_variant_inhabited(*index))
844                            .ok()?;
845                        variant_layouts[variant_id] =
846                            translate_variant_layout_data(&layout, variant_inhabited, vec![]);
847                    }
848                    r_abi::FieldsShape::Primitive | r_abi::FieldsShape::Array { .. } => {}
849                }
850                Some(Discriminator::trivial(variant_id))
851            }
852            r_abi::Variants::Empty => None,
853        };
854
855        Some(Layout {
856            size,
857            align,
858            discriminator,
859            inhabited,
860            variant_layouts,
861            repr,
862        })
863    }
864
865    /// Generate a naive layout for this type.
866    pub fn generate_naive_layout(&self, span: Span, ty: &TypeDeclKind) -> Result<Layout, Error> {
867        match ty {
868            TypeDeclKind::Struct(fields) => {
869                let mut size = 0;
870                let mut align = 0;
871                let ptr_size = self.translated.the_target_information().target_pointer_size;
872                let field_offsets = fields.map_ref(|field| {
873                    let offset = size;
874                    let size_of_ty = match field.ty.kind() {
875                        TyKind::Scalar(scalar_ty) => scalar_ty.target_size(ptr_size) as u64,
876                        // This is a lie, the pointers could be fat...
877                        TyKind::Ref(..) | TyKind::RawPtr(..) | TyKind::FnPtr(..) => ptr_size,
878                        _ => panic!("Unsupported type for `generate_naive_layout`: {ty:?}"),
879                    };
880                    size += size_of_ty;
881                    // For these types, align == size is good enough.
882                    align = std::cmp::max(align, size);
883                    OffsetExpr::new(offset)
884                });
885
886                Ok(Layout {
887                    size: Size::new(size),
888                    align: Size::new(align),
889                    discriminator: None,
890                    inhabited: InhabitedPredicate::mk_true(),
891                    variant_layouts: IndexVec::from([Some(VariantLayout {
892                        field_offsets,
893                        tagger: vec![],
894                        inhabited: InhabitedPredicate::mk_true(),
895                    })]),
896                    repr: ReprOptions::default(),
897                })
898            }
899            _ => raise_error!(
900                self,
901                span,
902                "`generate_naive_layout` only supports structs at the moment"
903            ),
904        }
905    }
906
907    /// Translate the body of a type declaration.
908    ///
909    /// Note that the type may be external, in which case we translate the body
910    /// only if it is public (i.e., it is a public enumeration, or it is a
911    /// struct with only public fields).
912    pub(crate) fn translate_adt_def(
913        &mut self,
914        trans_id: TypeDeclId,
915        def_span: Span,
916        item_meta: &ItemMeta,
917        def: &hax::FullDef<'tcx>,
918    ) -> Result<TypeDeclKind, Error> {
919        use crate::hax::AdtKind;
920        let hax::FullDefKind::Adt {
921            adt_kind, variants, ..
922        } = def.kind()
923        else {
924            unreachable!()
925        };
926
927        if item_meta.opacity.is_opaque() {
928            return Ok(TypeDeclKind::Opaque);
929        }
930
931        if matches!(adt_kind, AdtKind::Tuple) && self.t_ctx.options.no_gen_tuple_structs {
932            return Ok(TypeDeclKind::Opaque);
933        }
934
935        // hax's synthetic ADTs have no variants; we must construct the fields ourselves
936        let synthetic_fields = match adt_kind {
937            AdtKind::Tuple => {
938                let item = def.this();
939                let args = self.translate_generic_args(def_span, &item.generic_args, &[])?;
940                Some(args.types.into_iter().collect_vec())
941            }
942            AdtKind::Str => {
943                let u8_ty =
944                    TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::U8))).into_ty();
945                let u8_is_sized = self.translate_sized_proof(def_span, self.tcx.types.u8)?;
946                Some(vec![Ty::mk_slice(u8_ty, u8_is_sized)])
947            }
948            _ => None,
949        };
950        if let Some(tys) = synthetic_fields {
951            let fields = tys
952                .into_iter()
953                .enumerate()
954                .map(|(field_id, ty)| Field {
955                    span: def_span,
956                    attr_info: AttrInfo::dummy_public(),
957                    name: format!("_{field_id}"),
958                    is_positional: true,
959                    ty,
960                })
961                .collect();
962            return Ok(TypeDeclKind::Struct(fields));
963        }
964
965        trace!("{}", trans_id);
966
967        // In case the type is external, check if we should consider the type as
968        // transparent (i.e., extract its body). If it is an enumeration, then yes
969        // (because the variants of public enumerations are public, together with their
970        // fields). If it is a structure, we check if all the fields are public.
971        let contents_are_public = match adt_kind {
972            AdtKind::Enum => true,
973            AdtKind::Struct | AdtKind::Union => {
974                // Check the unique variant
975                error_assert!(self, def_span, variants.len() == 1);
976                variants[hax::VariantIdx::from(0usize)]
977                    .fields
978                    .iter()
979                    .all(|f| matches!(f.vis, Visibility::Public))
980            }
981            // The rest are fake adt kinds that won't reach here.
982            _ => unreachable!(),
983        };
984
985        if item_meta
986            .opacity
987            .with_content_visibility(contents_are_public)
988            .is_opaque()
989        {
990            return Ok(TypeDeclKind::Opaque);
991        }
992
993        // The type is transparent: explore the variants
994        let mut translated_variants: IndexVec<VariantId, Variant> = Default::default();
995        for (i, var_def) in variants.iter().enumerate() {
996            trace!("variant {i}: {var_def:?}");
997
998            let mut fields: IndexVec<FieldId, Field> = Default::default();
999            for (j, field_def) in var_def.fields.iter().enumerate() {
1000                trace!("variant {i}: field {j}: {field_def:?}");
1001                let field_span = self.t_ctx.translate_span(&field_def.span);
1002                // Translate the field type
1003                let ty = self.translate_ty(field_span, &field_def.ty)?;
1004                let field_full_def =
1005                    self.hax_def(&def.this().with_def_id(self.hax_state(), &field_def.did))?;
1006                let field_attrs = self.t_ctx.translate_attr_info(&field_full_def);
1007
1008                // Retrieve the field name.
1009                let is_positional = field_def.name.is_none();
1010                let field_name = field_def
1011                    .name
1012                    .map_or_else(|| format!("_{j}"), |name| name.to_string());
1013
1014                // Store the field
1015                let field = Field {
1016                    span: field_span,
1017                    attr_info: field_attrs,
1018                    name: field_name,
1019                    is_positional,
1020                    ty,
1021                };
1022                fields.push(field);
1023            }
1024
1025            let discriminant = self.translate_discriminant(def_span, &var_def.discr_val)?;
1026            let variant_span = self.t_ctx.translate_span(&var_def.span);
1027            let variant_name = var_def.name.to_string();
1028            let variant_full_def =
1029                self.hax_def(&def.this().with_def_id(self.hax_state(), &var_def.def_id))?;
1030
1031            let mut variant_attrs = self.t_ctx.translate_attr_info(&variant_full_def);
1032            // Propagate a `#[charon::variants_prefix(..)]` or `#[charon::variants_suffix(..)]` attribute to the variants.
1033            if variant_attrs.rename.is_none() {
1034                let prefix = item_meta
1035                    .attr_info
1036                    .attributes
1037                    .iter()
1038                    .filter_map(|a| a.as_variants_prefix())
1039                    .next()
1040                    .map(|attr| attr.as_str());
1041                let suffix = item_meta
1042                    .attr_info
1043                    .attributes
1044                    .iter()
1045                    .filter_map(|a| a.as_variants_suffix())
1046                    .next()
1047                    .map(|attr| attr.as_str());
1048                if prefix.is_some() || suffix.is_some() {
1049                    let prefix = prefix.unwrap_or_default();
1050                    let suffix = suffix.unwrap_or_default();
1051                    variant_attrs.rename = Some(format!("{prefix}{variant_name}{suffix}"));
1052                }
1053            }
1054
1055            translated_variants.push_with(|id| Variant {
1056                id,
1057                span: variant_span,
1058                attr_info: variant_attrs,
1059                name: variant_name,
1060                fields,
1061                discriminant,
1062            });
1063        }
1064
1065        // Register the type
1066        let type_def_kind: TypeDeclKind = match adt_kind {
1067            AdtKind::Struct => TypeDeclKind::Struct(translated_variants[0].fields.clone()),
1068            AdtKind::Enum => TypeDeclKind::Enum(translated_variants),
1069            AdtKind::Union => TypeDeclKind::Union(translated_variants[0].fields.clone()),
1070            // The rest are fake adt kinds that won't reach here.
1071            _ => unreachable!(),
1072        };
1073
1074        Ok(type_def_kind)
1075    }
1076
1077    fn translate_discriminant(
1078        &mut self,
1079        def_span: Span,
1080        discr: &hax::DiscriminantValue,
1081    ) -> Result<IntegerValue, Error> {
1082        let ty = self.translate_ty(def_span, &discr.ty)?;
1083        let scalar_ty = ty.kind().as_scalar().unwrap();
1084        match scalar_ty.as_integer() {
1085            Some(int_ty) => Ok(IntegerValue::from_bits(*int_ty, discr.val)),
1086            None => raise_error!(self, def_span, "unexpected discriminant type: {ty:?}",),
1087        }
1088    }
1089
1090    fn translate_inhabited_predicate(
1091        &mut self,
1092        span: Span,
1093        predicate: ty::inhabitedness::InhabitedPredicate<'tcx>,
1094    ) -> Result<InhabitedPredicate, Error> {
1095        use ty::inhabitedness::InhabitedPredicate as RustcPredicate;
1096        Ok(match predicate {
1097            RustcPredicate::True => InhabitedPredicateKind::True,
1098            RustcPredicate::False => InhabitedPredicateKind::False,
1099            RustcPredicate::ConstIsZero(value) => {
1100                InhabitedPredicateKind::ConstIsZero(self.translate_ty_constant_expr(span, &value)?)
1101            }
1102            // We only retain layout-relevant inhabitedness.
1103            RustcPredicate::NotInModule(_) => InhabitedPredicateKind::False,
1104            RustcPredicate::GenericType(ty) => {
1105                InhabitedPredicateKind::GenericType(self.translate_rustc_ty(span, &ty)?)
1106            }
1107            RustcPredicate::OpaqueType(key) => {
1108                // Reveal the opaque type.
1109                let opaque_ty = self
1110                    .tcx
1111                    .type_of(key.def_id)
1112                    .instantiate(self.tcx, key.args)
1113                    .skip_norm_wip();
1114                return self
1115                    .translate_inhabited_predicate(span, opaque_ty.inhabited_predicate(self.tcx));
1116            }
1117            RustcPredicate::And(&[left, right]) => InhabitedPredicateKind::And(vec![
1118                self.translate_inhabited_predicate(span, left)?,
1119                self.translate_inhabited_predicate(span, right)?,
1120            ]),
1121            RustcPredicate::Or(&[left, right]) => InhabitedPredicateKind::Or(vec![
1122                self.translate_inhabited_predicate(span, left)?,
1123                self.translate_inhabited_predicate(span, right)?,
1124            ]),
1125        }
1126        .into_pred())
1127    }
1128
1129    pub fn translate_repr_options(&mut self, hax_repr_options: &hax::ReprOptions) -> ReprOptions {
1130        let repr_algo = if hax_repr_options.flags.is_c {
1131            ReprAlgorithm::C
1132        } else {
1133            ReprAlgorithm::Rust
1134        };
1135
1136        let align_mod = if let Some(align) = &hax_repr_options.align {
1137            Some(AlignmentModifier::Align(align.bytes()))
1138        } else if let Some(pack) = &hax_repr_options.pack {
1139            Some(AlignmentModifier::Pack(pack.bytes()))
1140        } else {
1141            None
1142        };
1143
1144        let explicit_discr_type =
1145            hax_repr_options
1146                .int_specified
1147                .then(|| match hax_repr_options.typ.kind() {
1148                    hax::TyKind::Int(ty) => IntegerTy::Signed(Self::translate_hax_int_ty(ty)),
1149                    hax::TyKind::Uint(ty) => IntegerTy::Unsigned(Self::translate_hax_uint_ty(ty)),
1150                    ty => unreachable!("explicit enum discriminant type is not an integer: {ty:?}"),
1151                });
1152
1153        ReprOptions {
1154            transparent: hax_repr_options.flags.is_transparent,
1155            explicit_discr_type,
1156            repr_algo,
1157            align_modif: align_mod,
1158        }
1159    }
1160}
charon_driver/translate/translate_types.rs

charon_driver/translate/
translate_types.rs
