charon_driver/hax/types/
ty.rs

1//! Hax representations of Rust types and related type operations.
2
3use super::predicates::resolve_for_dyn;
4
5use crate::hax::prelude::*;
6
7use rustc_data_structures::intern::Interned;
8use rustc_middle::ty;
9use rustc_middle::ty::inherent::IntoKind;
10use rustc_span::def_id::DefId as RDefId;
11
12sinto_reexport!(rustc_abi::ExternAbi);
13
14/// Reflects [`rustc_middle::ty::Ty`]
15#[derive(Debug, Clone, PartialEq, Eq, Hash)]
16pub struct Ty<'tcx> {
17    pub(crate) kind: Interned<'tcx, TyKind<'tcx>>,
18}
19
20impl<'tcx> Ty<'tcx> {
21    pub fn new<S: BaseState<'tcx>>(s: &S, kind: TyKind<'tcx>) -> Self {
22        Ty {
23            kind: s.base().ty_interner.intern(kind),
24        }
25    }
26
27    pub fn kind(&self) -> &TyKind<'tcx> {
28        &self.kind
29    }
30
31    /// If this type represents something that implements the `Fn*` traits, return the
32    /// corresponding item.
33    pub fn callable_item(&self) -> Option<&ItemRef<'tcx>> {
34        match self.kind() {
35            TyKind::Closure(closure) => Some(&closure.item),
36            TyKind::FnDef(fn_def) => Some(&fn_def.item),
37            TyKind::FnPtr(fn_ptr) => Some(&fn_ptr.item),
38            _ => None,
39        }
40    }
41}
42
43impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Ty<'tcx>> for rustc_middle::ty::Ty<'tcx> {
44    fn sinto(&self, s: &S) -> Ty<'tcx> {
45        if let Some(ty) = s.with_cache(|cache| cache.tys.get(self).cloned()) {
46            return ty;
47        }
48        let kind: TyKind<'tcx> = self.kind().sinto(s);
49        let ty = Ty::new(s, kind);
50        s.with_cache(|cache| {
51            cache.tys.insert(*self, ty.clone());
52        });
53        ty
54    }
55}
56
57/// Reflects [`ty::TyKind`]
58#[derive(Debug, Clone, PartialEq, Eq, Hash)]
59pub enum TyKind<'tcx> {
60    Bool,
61    Char,
62    Int(IntTy),
63    Uint(UintTy),
64    Float(FloatTy),
65    FnDef(FnDefTy<'tcx>),
66    FnPtr(FnPtrTy<'tcx>),
67    Closure(ClosureTy<'tcx>),
68    Adt(AdtTy<'tcx>),
69    Foreign(ForeignTy<'tcx>),
70    Array(ArrayTy<'tcx>),
71    Pat(PatTy<'tcx>),
72    Slice(SliceTy<'tcx>),
73    Tuple(TupleTy<'tcx>),
74    Str(StrTy<'tcx>),
75    RawPtr(RawPtrTy<'tcx>),
76    Ref(RefTy<'tcx>),
77    DynTrait(DynTraitTy<'tcx>),
78    Coroutine(CoroutineTy<'tcx>),
79    Never,
80    Alias(Alias<'tcx>),
81    Param(ParamTy),
82    Bound(BoundTyRef),
83    Placeholder(PlaceholderTy),
84    Infer(InferTy),
85    Error,
86    Todo(String),
87}
88
89impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, TyKind<'tcx>> for ty::TyKind<'tcx> {
90    #[tracing::instrument(level = "trace", skip(s))]
91    fn sinto(&self, s: &S) -> TyKind<'tcx> {
92        let base = s.base();
93        let tcx = base.tcx;
94        match self {
95            Self::Bool => TyKind::Bool,
96            Self::Char => TyKind::Char,
97            Self::Int(int_ty) => TyKind::Int(int_ty.sinto(s)),
98            Self::Uint(uint_ty) => TyKind::Uint(uint_ty.sinto(s)),
99            Self::Float(float_ty) => TyKind::Float(float_ty.sinto(s)),
100            Self::FnDef(fun_id, generics) => {
101                // Note: loss of precision, we erase the bound vars.
102                let generics = tcx.instantiate_bound_regions_with_erased(*generics);
103                TyKind::FnDef(FnDefTy {
104                    item: translate_item_ref(s, *fun_id, generics),
105                })
106            }
107            Self::FnPtr(tys, header) => {
108                let sig = tys.with(*header);
109                let item = ItemRef::translate_fn_ptr(s, sig);
110                TyKind::FnPtr(FnPtrTy {
111                    sig: Box::new(sig.sinto(s)),
112                    item,
113                })
114            }
115            Self::Closure(def_id, generics) => {
116                TyKind::Closure(ClosureTy::sfrom(s, *def_id, generics))
117            }
118            Self::Adt(adt_def, generics) => TyKind::Adt(AdtTy {
119                item: translate_item_ref(s, adt_def.did(), generics),
120            }),
121            Self::Foreign(def_id) => TyKind::Foreign(ForeignTy {
122                item: translate_item_ref(s, *def_id, Default::default()),
123            }),
124            Self::Array(ty, len) => {
125                let args = tcx.mk_args(&[(*ty).into(), (*len).into()]);
126                let sized_trait = tcx.lang_items().sized_trait().unwrap();
127                TyKind::Array(ArrayTy {
128                    item: ItemRef::translate_synthetic(s, SyntheticItem::Array, args),
129                    has_sized_proof: !base
130                        .elab_ctx
131                        .bounds_options()
132                        .remove_traits
133                        .contains(&sized_trait),
134                })
135            }
136            Self::Pat(ty, pat) => TyKind::Pat(PatTy {
137                ty: ty.sinto(s),
138                pat: pat.sinto(s),
139            }),
140            Self::Slice(ty) => {
141                let args = tcx.mk_args(&[(*ty).into()]);
142                let sized_trait = tcx.lang_items().sized_trait().unwrap();
143                TyKind::Slice(SliceTy {
144                    item: ItemRef::translate_synthetic(s, SyntheticItem::Slice, args),
145                    has_sized_proof: !base
146                        .elab_ctx
147                        .bounds_options()
148                        .remove_traits
149                        .contains(&sized_trait),
150                })
151            }
152            Self::Tuple(tys) => {
153                let args = tcx.mk_args_from_iter(tys.into_iter().map(ty::GenericArg::from));
154                TyKind::Tuple(TupleTy {
155                    item: ItemRef::translate_synthetic(s, SyntheticItem::Tuple(tys.len()), args),
156                })
157            }
158            Self::Str => {
159                let args = tcx.mk_args(&[]);
160                TyKind::Str(StrTy {
161                    item: ItemRef::translate_synthetic(s, SyntheticItem::Str, args),
162                })
163            }
164            Self::RawPtr(ty, mutbl) => TyKind::RawPtr(RawPtrTy {
165                ty: ty.sinto(s),
166                mutbl: mutbl.sinto(s),
167            }),
168            Self::Ref(region, ty, mutbl) => TyKind::Ref(RefTy {
169                region: region.sinto(s),
170                ty: ty.sinto(s),
171                mutbl: mutbl.sinto(s),
172            }),
173            Self::Dynamic(preds, region) => TyKind::DynTrait(DynTraitTy {
174                binder: resolve_for_dyn(s, preds, |_, _| ()),
175                region: region.sinto(s),
176            }),
177            Self::Coroutine(def_id, generics) => TyKind::Coroutine(CoroutineTy {
178                item: translate_item_ref(s, *def_id, generics),
179            }),
180            Self::Never => TyKind::Never,
181            Self::Alias(_, alias_ty) => Alias::from(s, alias_ty),
182            Self::Param(param) => TyKind::Param(param.sinto(s)),
183            Self::Bound(index, ty) => TyKind::Bound(BoundTyRef {
184                index: index.sinto(s),
185                ty: ty.sinto(s),
186            }),
187            Self::Placeholder(placeholder) => TyKind::Placeholder(placeholder.sinto(s)),
188            Self::Infer(infer) => TyKind::Infer(infer.sinto(s)),
189            Self::Error(..) => TyKind::Error,
190            other => TyKind::Todo(format!("{other:?}")),
191        }
192    }
193}
194
195#[derive(Debug, Clone, PartialEq, Eq, Hash)]
196pub struct FnDefTy<'tcx> {
197    pub item: ItemRef<'tcx>,
198}
199
200#[derive(Debug, Clone, PartialEq, Eq, Hash)]
201pub struct FnPtrTy<'tcx> {
202    pub sig: Box<PolyFnSig<'tcx>>,
203    /// Points to a synthetic item used to build impls for function pointer types.
204    pub item: ItemRef<'tcx>,
205}
206
207/// Reflects [`ty::ClosureArgs`]
208#[derive(Debug, Clone, PartialEq, Eq, Hash)]
209pub struct ClosureTy<'tcx> {
210    pub item: ItemRef<'tcx>,
211}
212
213impl<'tcx> ClosureTy<'tcx> {
214    /// The base kind of this closure. The kinds are ordered by inclusion: any `Fn` works as an
215    /// `FnMut`, and any `FnMut` works as an `FnOnce`.
216    pub fn kind(&self, s: &impl BaseState<'tcx>) -> ClosureKind {
217        let s = &s.with_hax_owner(&self.item.def_id);
218        self.item.rustc_args(s).as_closure().kind().sinto(s)
219    }
220
221    /// The signature of the function that this closure implements, e.g. `fn(A, B, C) -> D`.
222    pub fn fn_sig(&self, s: &impl BaseState<'tcx>) -> PolyFnSig<'tcx> {
223        let s = &s.with_hax_owner(&self.item.def_id);
224        let args = self.item.rustc_args(s);
225        closure_sig(s.tcx(), args.as_closure()).sinto(s)
226    }
227
228    // Manual implementation because we need the `def_id` of the closure.
229    pub fn sfrom<S>(s: &S, def_id: RDefId, from: ty::GenericArgsRef<'tcx>) -> Self
230    where
231        S: UnderOwnerState<'tcx>,
232    {
233        let item = translate_item_ref(s, def_id, from);
234        ClosureTy { item }
235    }
236}
237
238#[derive(Debug, Clone, PartialEq, Eq, Hash)]
239pub struct AdtTy<'tcx> {
240    pub item: ItemRef<'tcx>,
241}
242
243#[derive(Debug, Clone, PartialEq, Eq, Hash)]
244pub struct ForeignTy<'tcx> {
245    pub item: ItemRef<'tcx>,
246}
247
248#[derive(Debug, Clone, PartialEq, Eq, Hash)]
249pub struct ArrayTy<'tcx> {
250    pub item: ItemRef<'tcx>,
251    has_sized_proof: bool,
252}
253
254impl<'tcx> ArrayTy<'tcx> {
255    /// The `Sized` proof for the element type, if we're not hiding `Sized`.
256    pub fn element_sized_proof(&self) -> Option<&TraitProof<'tcx>> {
257        if self.has_sized_proof {
258            Some(&self.item.trait_proofs[0])
259        } else {
260            None
261        }
262    }
263}
264
265#[derive(Debug, Clone, PartialEq, Eq, Hash)]
266pub struct PatTy<'tcx> {
267    pub ty: Ty<'tcx>,
268    pub pat: Pattern<'tcx>,
269}
270
271#[derive(Debug, Clone, PartialEq, Eq, Hash)]
272pub struct SliceTy<'tcx> {
273    pub item: ItemRef<'tcx>,
274    has_sized_proof: bool,
275}
276
277impl<'tcx> SliceTy<'tcx> {
278    /// The `Sized` proof for the element type, if we're not hiding `Sized`.
279    pub fn element_sized_proof(&self) -> Option<&TraitProof<'tcx>> {
280        if self.has_sized_proof {
281            Some(&self.item.trait_proofs[0])
282        } else {
283            None
284        }
285    }
286}
287
288#[derive(Debug, Clone, PartialEq, Eq, Hash)]
289pub struct TupleTy<'tcx> {
290    pub item: ItemRef<'tcx>,
291}
292
293#[derive(Debug, Clone, PartialEq, Eq, Hash)]
294pub struct StrTy<'tcx> {
295    pub item: ItemRef<'tcx>,
296}
297
298#[derive(Debug, Clone, PartialEq, Eq, Hash)]
299pub struct RawPtrTy<'tcx> {
300    pub ty: Ty<'tcx>,
301    pub mutbl: Mutability,
302}
303
304#[derive(Debug, Clone, PartialEq, Eq, Hash)]
305pub struct RefTy<'tcx> {
306    pub region: Region,
307    pub ty: Ty<'tcx>,
308    pub mutbl: Mutability,
309}
310
311#[derive(Debug, Clone, PartialEq, Eq, Hash)]
312pub struct DynTraitTy<'tcx> {
313    pub binder: DynBinder<'tcx, ()>,
314    pub region: Region,
315}
316
317impl<'tcx> DynTraitTy<'tcx> {
318    /// The principal trait clause, if any.
319    pub fn principal_trait_clause(&self) -> Option<&Binder<ClauseKind<'tcx>>> {
320        let clause = &self.binder.predicates.predicates.first()?.clause.kind;
321        if matches!(clause.hax_skip_binder_ref(), ClauseKind::Trait(_)) {
322            Some(clause)
323        } else {
324            None
325        }
326    }
327}
328
329#[derive(Debug, Clone, PartialEq, Eq, Hash)]
330pub struct CoroutineTy<'tcx> {
331    pub item: ItemRef<'tcx>,
332}
333
334/// Reflects [`ty::UserSelfTy`]
335#[derive(Debug, Clone, AdtInto)]
336#[args(< S: UnderOwnerState<'tcx>>, from: ty::UserSelfTy<'tcx>, state: S as gstate)]
337pub struct UserSelfTy<'tcx> {
338    pub impl_def_id: DefId,
339    pub self_ty: Ty<'tcx>,
340}
341
342/// Reflects [`ty::UserArgs`]
343#[derive(Debug, Clone, AdtInto)]
344#[args(< S: UnderOwnerState<'tcx>>, from: ty::UserArgs<'tcx>, state: S as gstate)]
345pub struct UserArgs<'tcx> {
346    pub args: Vec<GenericArg<'tcx>>,
347    pub user_self_ty: Option<UserSelfTy<'tcx>>,
348}
349
350/// Reflects [`ty::UserType`]: this is currently
351/// disabled, and everything is printed as debug in the
352/// [`UserType::Todo`] variant.
353#[derive(Debug, Clone, AdtInto)]
354#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::UserType<'tcx>, state: S as _s)]
355pub enum UserType {
356    // TODO: for now, we don't use user types at all.
357    // We disable it for now, since it cause the following to fail:
358    //
359    //    pub const MY_VAL: u16 = 5;
360    //    pub type Alias = MyStruct<MY_VAL>; // Using the literal 5, it goes through
361    //
362    //    pub struct MyStruct<const VAL: u16> {}
363    //
364    //    impl<const VAL: u16> MyStruct<VAL> {
365    //        pub const MY_CONST: u16 = VAL;
366    //    }
367    //
368    //    pub fn do_something() -> u32 {
369    //        u32::from(Alias::MY_CONST)
370    //    }
371    //
372    // In this case, we get a [ty::ConstKind::Bound] in
373    // [do_something], which we are not able to translate.
374    // See: https://github.com/hacspec/hax/pull/209
375
376    // Ty(Ty),
377    // TypeOf(DefId, UserArgs),
378    #[todo]
379    Todo(String),
380}
381
382/// Reflects [`rustc_ast::ast::LitIntType`]
383#[derive(AdtInto)]
384#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitIntType, state: S as gstate)]
385#[derive(Debug, Clone, PartialEq, Eq, Hash)]
386pub enum LitIntType {
387    Signed(IntTy),
388    Unsigned(UintTy),
389    Unsuffixed,
390}
391
392/// Reflects [`ty::IntTy`]
393#[derive(AdtInto)]
394#[args(<S>, from: ty::IntTy, state: S as _s)]
395#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
396pub enum IntTy {
397    Isize,
398    I8,
399    I16,
400    I32,
401    I64,
402    I128,
403}
404
405/// Reflects [`ty::FloatTy`]
406#[derive(AdtInto)]
407#[args(<S>, from: ty::FloatTy, state: S as _s)]
408#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
409pub enum FloatTy {
410    F16,
411    F32,
412    F64,
413    F128,
414}
415
416/// Reflects [`ty::UintTy`]
417#[derive(AdtInto)]
418#[args(<S>, from: ty::UintTy, state: S as _s)]
419#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
420pub enum UintTy {
421    Usize,
422    U8,
423    U16,
424    U32,
425    U64,
426    U128,
427}
428
429#[allow(clippy::to_string_trait_impl)]
430impl ToString for IntTy {
431    fn to_string(&self) -> String {
432        use IntTy::*;
433        match self {
434            Isize => "isize".to_string(),
435            I8 => "i8".to_string(),
436            I16 => "i16".to_string(),
437            I32 => "i32".to_string(),
438            I64 => "i64".to_string(),
439            I128 => "i128".to_string(),
440        }
441    }
442}
443
444#[allow(clippy::to_string_trait_impl)]
445impl ToString for UintTy {
446    fn to_string(&self) -> String {
447        use UintTy::*;
448        match self {
449            Usize => "usize".to_string(),
450            U8 => "u8".to_string(),
451            U16 => "u16".to_string(),
452            U32 => "u32".to_string(),
453            U64 => "u64".to_string(),
454            U128 => "u128".to_string(),
455        }
456    }
457}
458
459/// Reflects [`ty::TypeAndMut`]
460#[derive(AdtInto)]
461#[args(< S: UnderOwnerState<'tcx>>, from: ty::TypeAndMut<'tcx>, state: S as gstate)]
462#[derive(Debug, Clone, PartialEq, Eq, Hash)]
463pub struct TypeAndMut<'tcx> {
464    pub ty: Ty<'tcx>,
465    pub mutbl: Mutability,
466}
467
468impl<S, U, T: SInto<S, U>> SInto<S, Vec<U>> for ty::List<T> {
469    fn sinto(&self, s: &S) -> Vec<U> {
470        self.iter().map(|x| x.sinto(s)).collect()
471    }
472}
473
474/// This type merges the information from
475/// [`ty::AliasTyKind`] and [`ty::AliasTy`].
476#[derive(Debug, Clone, PartialEq, Eq, Hash)]
477pub struct Alias<'tcx> {
478    pub kind: AliasKind<'tcx>,
479    pub args: Vec<GenericArg<'tcx>>,
480    pub def_id: DefId,
481}
482
483/// Reflects [`rustc_middle::ty::AliasTyKind`].
484#[derive(Debug, Clone, PartialEq, Eq, Hash)]
485pub enum AliasKind<'tcx> {
486    /// The projection of a trait type: `<Ty as Trait<...>>::Type<...>`
487    Projection(ItemRef<'tcx>),
488    /// An associated type in an inherent impl.
489    Inherent,
490    /// An `impl Trait` opaque type.
491    Opaque {
492        /// The real type hidden inside this opaque type.
493        hidden_ty: Ty<'tcx>,
494    },
495    /// A type alias that references opaque types. Likely to always be normalized away.
496    Free,
497}
498
499pub fn alias_ty_kind_def_id<'tcx>(kind: ty::AliasTyKind<'tcx>) -> RDefId {
500    match kind {
501        ty::AliasTyKind::Projection { def_id }
502        | ty::AliasTyKind::Inherent { def_id }
503        | ty::AliasTyKind::Opaque { def_id }
504        | ty::AliasTyKind::Free { def_id } => def_id,
505    }
506}
507
508impl<'tcx> Alias<'tcx> {
509    #[tracing::instrument(level = "trace", skip(s))]
510    fn from<S: UnderOwnerState<'tcx>>(s: &S, alias_ty: &ty::AliasTy<'tcx>) -> TyKind<'tcx> {
511        let tcx = s.base().tcx;
512        let typing_env = s.typing_env();
513        use ty::AliasTyKind as RustAliasKind;
514
515        // Try to normalize the alias first.
516        let ty = ty::Ty::new_alias(tcx, ty::IsRigid::No, *alias_ty);
517        let ty = normalize(tcx, typing_env, ty::Unnormalized::new(ty));
518        let ty::Alias(_is_rigid, alias_ty) = ty.kind() else {
519            let ty: Ty = ty.sinto(s);
520            return ty.kind().clone();
521        };
522
523        let kind = match alias_ty.kind {
524            RustAliasKind::Projection { def_id } => {
525                AliasKind::Projection(ItemRef::translate_projection(s, def_id, alias_ty.args))
526            }
527            RustAliasKind::Inherent { .. } => AliasKind::Inherent,
528            RustAliasKind::Opaque { def_id } => {
529                // Reveal the underlying `impl Trait` type.
530                let ty = tcx.type_of(def_id).instantiate(tcx, alias_ty.args);
531                let ty = normalize(tcx, s.typing_env(), ty);
532                AliasKind::Opaque {
533                    hidden_ty: ty.sinto(s),
534                }
535            }
536            RustAliasKind::Free { .. } => AliasKind::Free,
537        };
538        TyKind::Alias(Alias {
539            kind,
540            args: alias_ty.args.sinto(s),
541            def_id: alias_ty_kind_def_id(alias_ty.kind).sinto(s),
542        })
543    }
544}
545
546#[derive(AdtInto)]
547#[args(< S: UnderOwnerState<'tcx>>, from: ty::pattern::PatternKind<'tcx>, state: S as gstate)]
548#[derive(Debug, Clone, PartialEq, Eq, Hash)]
549pub enum Pattern<'tcx> {
550    Range {
551        start: ConstantExpr<'tcx>,
552        end: ConstantExpr<'tcx>,
553    },
554    Or(Vec<Pattern<'tcx>>),
555    NotNull,
556}
557
558impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Pattern<'tcx>> for ty::Pattern<'tcx> {
559    fn sinto(&self, s: &S) -> Pattern<'tcx> {
560        self.kind().sinto(s)
561    }
562}
563/// Reflects [`ty::CanonicalUserTypeAnnotation`]
564#[derive(AdtInto)]
565#[args(< S: UnderOwnerState<'tcx>>, from: ty::CanonicalUserTypeAnnotation<'tcx>, state: S as gstate)]
566#[derive(Debug, Clone)]
567pub struct CanonicalUserTypeAnnotation<'tcx> {
568    pub user_ty: CanonicalUserType,
569    pub span: Span,
570    pub inferred_ty: Ty<'tcx>,
571}
572
573/// The metadata to attach to the newly-unsized ptr.
574#[derive(Debug, Clone, PartialEq, Eq, Hash)]
575pub enum UnsizingMetadata<'tcx> {
576    /// Unsize an array to a slice, storing the length as metadata.
577    Length(ConstantExpr<'tcx>),
578    /// Unsize a non-dyn type to a dyn type, adding a vtable pointer as metadata.
579    DirectVTable(TraitProof<'tcx>),
580    /// Unsize a dyn-type to another dyn-type, (optionally) indexing within the current vtable.
581    NestedVTable(DynBinder<'tcx, TraitProof<'tcx>>),
582    /// Couldn't compute
583    Unknown,
584}
585
586pub fn compute_unsizing_metadata<'tcx, S: UnderOwnerState<'tcx>>(
587    s: &S,
588    src_ty: ty::Ty<'tcx>,
589    tgt_ty: ty::Ty<'tcx>,
590) -> (Vec<FieldIdx>, UnsizingMetadata<'tcx>) {
591    let tcx = s.base().tcx;
592    // Unless boxes are built-in, we go through their fields like for other smart pointers.
593    let builtin_deref = |ty: ty::Ty<'tcx>| {
594        (!ty.is_box() || s.base().options.treat_box_as_builtin)
595            .then(|| ty.builtin_deref(true))
596            .flatten()
597    };
598    let (Some(src_ty), Some(tgt_ty)) = (builtin_deref(src_ty), builtin_deref(tgt_ty)) else {
599        // Like `rustc_monomorphize::custom_coerce_unsize_info`: for a `CoerceUnsized` struct
600        // (e.g. `Rc`), find the impl and recurse into the field it coerces.
601        return match (src_ty.kind(), tgt_ty.kind()) {
602            (ty::Adt(def, src_args), ty::Adt(_, tgt_args)) => {
603                let coerce_trait = tcx.lang_items().coerce_unsized_trait().unwrap();
604                let tref = ty::TraitRef::new(tcx, coerce_trait, [src_ty, tgt_ty]);
605                let proof =
606                    s.with_predicate_searcher(|ps, ctx| ps.resolve(ctx, &ty::Binder::dummy(tref)));
607                let elaboration::TraitProofKind::Concrete(impl_ref) = &proof.contents().kind else {
608                    unreachable!("`CoerceUnsized` between ADTs is always proven by a concrete impl")
609                };
610                let info = tcx
611                    .coerce_unsized_info(impl_ref.def_id.real_rust_def_id())
612                    .unwrap();
613                let ty::adjustment::CustomCoerceUnsized::Struct(i) = info.custom_kind.unwrap();
614                let field = &def.non_enum_variant().fields[i];
615                let typing_env = s.typing_env();
616                let src_ty = normalize(tcx, typing_env, field.ty(tcx, src_args));
617                let tgt_ty = normalize(tcx, typing_env, field.ty(tcx, tgt_args));
618                let (mut path, meta) = compute_unsizing_metadata(s, src_ty, tgt_ty);
619                path.insert(0, i);
620                (path, meta)
621            }
622            (ty::Pat(a, _), ty::Pat(b, _)) => compute_unsizing_metadata(s, *a, *b),
623            _ => (vec![], UnsizingMetadata::Unknown),
624        };
625    };
626    let typing_env = s.typing_env();
627    let (src_ty, tgt_ty) =
628        tcx.struct_lockstep_tails_raw(src_ty, tgt_ty, |ty| normalize(tcx, typing_env, ty));
629
630    let meta = match (&src_ty.kind(), &tgt_ty.kind()) {
631        (ty::Array(_, len), ty::Slice(_) | ty::Str) => {
632            let len = len.sinto(s);
633            UnsizingMetadata::Length(len)
634        }
635        (ty::Dynamic(from_preds, _), ty::Dynamic(to_preds, ..)) => {
636            let trait_proof = resolve_for_dyn(s, from_preds, |searcher, fresh_ty| {
637                let to_pred = if let Some(to_principal) = to_preds.principal() {
638                    to_principal.with_self_ty(tcx, fresh_ty)
639                } else {
640                    let def_id = to_preds
641                        .iter()
642                        .find_map(|pred| match pred.skip_binder() {
643                            ty::ExistentialPredicate::AutoTrait(def_id) => Some(def_id),
644                            _ => None,
645                        })
646                        .expect("expected a trait predicate in dyn upcast target");
647                    ty::Binder::dummy(ty::TraitRef::new(tcx, def_id, [fresh_ty]))
648                };
649                searcher.resolve(&s.base_state(), &to_pred)
650            });
651            UnsizingMetadata::NestedVTable(trait_proof)
652        }
653        (_, ty::Dynamic(preds, ..)) => {
654            let pred = preds[0].with_self_ty(tcx, src_ty);
655            let clause = pred.as_trait_clause().expect(
656                "the first `ExistentialPredicate` of `TyKind::Dynamic` \\
657                                        should be a trait clause",
658            );
659            let tref = clause.rebind(clause.skip_binder().trait_ref);
660            let trait_proof = solve_trait(s, tref);
661
662            UnsizingMetadata::DirectVTable(trait_proof)
663        }
664        _ => UnsizingMetadata::Unknown,
665    };
666    (vec![], meta)
667}
668
669/// Reflects [`ty::FnSig`]
670#[derive(Debug, Clone, PartialEq, Eq, Hash)]
671#[derive(AdtInto)]
672#[args(< S: UnderOwnerState<'tcx>>, from: ty::FnSig<'tcx>, state: S as s)]
673pub struct TyFnSig<'tcx> {
674    #[value(self.inputs().sinto(s))]
675    pub inputs: Vec<Ty<'tcx>>,
676    /// The inputs tupled as the `Fn*` traits take them, e.g. `(A, B, C)`.
677    #[value(ty::Ty::new_tup(s.base().tcx, self.inputs()).sinto(s))]
678    pub tupled_inputs: Ty<'tcx>,
679    #[value(self.output().sinto(s))]
680    pub output: Ty<'tcx>,
681    #[value(self.c_variadic())]
682    pub c_variadic: bool,
683    #[value(self.safety())]
684    pub safety: Safety,
685    #[value(self.abi())]
686    pub abi: ExternAbi,
687}
688
689/// Reflects [`ty::PolyFnSig`]
690pub type PolyFnSig<'tcx> = Binder<TyFnSig<'tcx>>;
691
692/// Retrieve a closure's signature.
693pub fn closure_sig<'tcx>(
694    tcx: ty::TyCtxt<'tcx>,
695    closure: ty::ClosureArgs<ty::TyCtxt<'tcx>>,
696) -> ty::PolyFnSig<'tcx> {
697    tcx.signature_unclosure(closure.sig(), rustc_hir::Safety::Safe)
698}
699
700/// Reflects [`ty::ClosureKind`]
701#[derive(AdtInto)]
702#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::ClosureKind, state: S as _tcx)]
703#[derive(Debug, Clone, PartialEq, Eq, Hash)]
704pub enum ClosureKind {
705    Fn,
706    FnMut,
707    FnOnce,
708}
charon_driver/hax/types/ty.rs

charon_driver/hax/types/
ty.rs
