charon_driver/hax/types/
traits.rs

1use crate::hax::prelude::*;
2
3use rustc_middle::ty;
4
5/// Reflects [`ty::TraitRef`]
6/// Contains the def_id and arguments passed to the trait. The first type argument is the `Self`
7/// type. The trait proofs are the _required_ predicate for this trait; currently they are always
8/// empty because we consider all trait predicates as implied.
9/// `self.in_trait` is always `None` because a trait can't be associated to another one.
10pub type TraitRef<'tcx> = ItemRef<'tcx>;
11
12impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, TraitRef<'tcx>> for ty::TraitRef<'tcx> {
13    fn sinto(&self, s: &S) -> TraitRef<'tcx> {
14        translate_item_ref(s, self.def_id, self.args)
15    }
16}
17
18/// Reflects [`ty::AssocItem`]
19#[derive(Debug, Clone, PartialEq, Eq, Hash)]
20pub struct AssocItem<'tcx> {
21    pub def_id: DefId,
22    /// This is `None` for RPTITs.
23    pub name: Option<Symbol>,
24    pub kind: AssocKind,
25    pub container: AssocItemContainer<'tcx>,
26    /// Whether this item has a value (e.g. this is `false` for trait methods without default
27    /// implementations).
28    pub has_value: bool,
29}
30
31impl<'tcx> AssocItem<'tcx> {
32    pub fn sfrom<S: BaseState<'tcx>>(s: &S, item: &ty::AssocItem) -> AssocItem<'tcx> {
33        Self::sfrom_instantiated(s, item, None)
34    }
35
36    /// Translate an `AssocItem` and optionally instantiate it with the provided arguments.
37    pub fn sfrom_instantiated<S: BaseState<'tcx>>(
38        s: &S,
39        item: &ty::AssocItem,
40        item_args: Option<ty::GenericArgsRef<'tcx>>,
41    ) -> AssocItem<'tcx> {
42        let tcx = s.base().tcx;
43        // We want to solve traits in the context of this item.
44        let item_def_id = item.def_id.sinto(s);
45        let s = &s.with_hax_owner(&item_def_id);
46        let item_args = item_args.unwrap_or_else(|| item_def_id.identity_args(s));
47        let container_id = item.container_id(tcx);
48        let container_args = item_args.truncate_to(tcx, tcx.generics_of(container_id));
49        let container = match item.container {
50            ty::AssocContainer::Trait => {
51                let trait_ref =
52                    ty::TraitRef::new_from_args(tcx, container_id, container_args).sinto(s);
53                AssocItemContainer::TraitContainer { trait_ref }
54            }
55            ty::AssocContainer::TraitImpl(implemented_item_id) => {
56                let implemented_item_id = implemented_item_id.unwrap();
57                let item = translate_item_ref(s, container_id, container_args);
58                let implemented_trait_ref = tcx
59                    .impl_trait_ref(container_id)
60                    .instantiate(tcx, container_args);
61                let implemented_trait_ref = normalize(tcx, s.typing_env(), implemented_trait_ref);
62                let implemented_trait_item = {
63                    let implemented_item_id = implemented_item_id.sinto(s);
64                    let generics =
65                        item_args.rebase_onto(tcx, container_id, implemented_trait_ref.args);
66                    // Don't resolve, otherwise we'll always get the impl item id back.
67                    ItemRef::translate_from_hax_def_id_maybe_resolve(
68                        s,
69                        implemented_item_id,
70                        generics,
71                        AssocItemResolution::None,
72                    )
73                };
74                AssocItemContainer::TraitImplContainer {
75                    impl_: item,
76                    implemented_trait_ref: implemented_trait_ref.sinto(s),
77                    implemented_trait_item,
78                    overrides_default: tcx.defaultness(implemented_item_id).has_value(),
79                }
80            }
81            ty::AssocContainer::InherentImpl => AssocItemContainer::InherentImplContainer {
82                impl_id: container_id.sinto(s),
83                self_ty: inst_binder(
84                    tcx,
85                    s.typing_env(),
86                    Some(container_args),
87                    tcx.type_of(container_id),
88                )
89                .sinto(s),
90            },
91        };
92        let name = match item.opt_name() {
93            None if let ty::AssocKind::Type { data } = item.kind
94                && let ty::AssocTypeData::Rpitit(rpitit) = data =>
95            {
96                let (ty::ImplTraitInTraitData::Trait { fn_def_id, .. }
97                | ty::ImplTraitInTraitData::Impl { fn_def_id, .. }) = rpitit;
98                let fn_name = tcx.item_name(fn_def_id);
99                let name = Symbol::intern(&format!("{fn_name}_ty"));
100                Some(name)
101            }
102            opt_name => opt_name,
103        };
104        AssocItem {
105            def_id: item.def_id.sinto(s),
106            name,
107            kind: item.kind.sinto(s),
108            container,
109            has_value: item.defaultness(tcx).has_value(),
110        }
111    }
112
113    /// The `DefId` of the item being implemented.
114    pub fn implemented_trait_item_id(&self) -> &DefId {
115        match &self.container {
116            AssocItemContainer::TraitImplContainer {
117                implemented_trait_item,
118                ..
119            } => &implemented_trait_item.def_id,
120            _ => &self.def_id,
121        }
122    }
123}
124
125/// Reflects [`ty::AssocKind`]
126#[derive(AdtInto)]
127#[args(<'tcx, S: BaseState<'tcx>>, from: ty::AssocKind, state: S as _tcx)]
128#[derive(Debug, Clone, PartialEq, Eq, Hash)]
129pub enum AssocKind {
130    Const { name: Symbol },
131    Fn { name: Symbol, has_self: bool },
132    Type { data: AssocTypeData },
133}
134
135/// Reflects [`ty::AssocTypeData`]
136#[derive(AdtInto)]
137#[args(<'tcx, S: BaseState<'tcx>>, from: ty::AssocTypeData, state: S as _tcx)]
138#[derive(Debug, Clone, PartialEq, Eq, Hash)]
139pub enum AssocTypeData {
140    Normal(Symbol),
141    Rpitit(ImplTraitInTraitData),
142}
143
144#[derive(Debug, Clone, PartialEq, Eq, Hash)]
145pub enum AssocItemContainer<'tcx> {
146    TraitContainer {
147        trait_ref: TraitRef<'tcx>,
148    },
149    TraitImplContainer {
150        /// Reference to the def_id of the impl block.
151        impl_: ItemRef<'tcx>,
152        /// The trait ref implemented by the impl block.
153        implemented_trait_ref: TraitRef<'tcx>,
154        /// The the associated item (in the trait declaration) that is being implemented.
155        implemented_trait_item: ItemRef<'tcx>,
156        /// Whether the corresponding trait item had a default (and therefore this one overrides
157        /// it).
158        overrides_default: bool,
159    },
160    InherentImplContainer {
161        impl_id: DefId,
162        /// The self type instantiated with this associated item's arguments.
163        self_ty: Ty<'tcx>,
164    },
165}
166
167/// Reflects [`ty::ImplTraitInTraitData`]
168#[derive(AdtInto)]
169#[args(<'tcx, S: BaseState<'tcx>>, from: ty::ImplTraitInTraitData, state: S as _s)]
170#[derive(Debug, Clone, PartialEq, Eq, Hash)]
171pub enum ImplTraitInTraitData {
172    Trait {
173        fn_def_id: DefId,
174        opaque_def_id: DefId,
175    },
176    Impl {
177        fn_def_id: DefId,
178    },
179}
charon_driver/hax/types/traits.rs

charon_driver/hax/types/
traits.rs
