charon_driver/hax/
traits.rs

1use rustc_middle::ty;
2use rustc_span::def_id::DefId as RDefId;
3
4pub use rustc_trait_elaboration as elaboration;
5pub use rustc_trait_elaboration::{
6    ItemPredicate, ItemPredicateId, ItemPredicates, PredicateSearcher, ToPolyTraitRef,
7    erase_and_norm, erase_free_regions, normalize, self_predicate,
8};
9
10use crate::hax::prelude::*;
11use charon_lib::ast::HashConsed;
12
13#[derive(Clone, Debug, Hash, PartialEq, Eq)]
14pub enum ImplExprPathChunk {
15    AssocItem {
16        /// Reference to the item, with generics (for GATs), e.g. the `T` and `T: Clone` `ImplExpr`
17        /// in the following example:
18        /// ```ignore
19        /// trait Foo {
20        ///     type Type<T: Clone>: Debug;
21        /// }
22        /// ```
23        item: ItemRef,
24        /// The implemented predicate.
25        predicate: Binder<TraitRef>,
26        /// The index of this predicate in the list returned by `ItemPredicates::Implied`.
27        index: usize,
28    },
29    Parent {
30        /// The implemented predicate.
31        predicate: Binder<TraitRef>,
32        /// The index of this predicate in the list returned by `ItemPredicates::Implied`.
33        index: usize,
34    },
35}
36
37impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ImplExprPathChunk> for elaboration::PathChunk<'tcx> {
38    fn sinto(&self, s: &S) -> ImplExprPathChunk {
39        match self {
40            elaboration::PathChunk::AssocItem {
41                item,
42                predicate,
43                index,
44                ..
45            } => ImplExprPathChunk::AssocItem {
46                item: item.sinto(s),
47                predicate: predicate.sinto(s),
48                index: index.sinto(s),
49            },
50            elaboration::PathChunk::Parent {
51                predicate, index, ..
52            } => ImplExprPathChunk::Parent {
53                predicate: predicate.sinto(s),
54                index: index.sinto(s),
55            },
56        }
57    }
58}
59
60/// The source of a particular trait implementation. Most often this is either `Concrete` for a
61/// concrete `impl Trait for Type {}` item, or `LocalBound` for a context-bound `where T: Trait`.
62#[derive(AdtInto)]
63#[args(<'tcx, S: UnderOwnerState<'tcx> >, from: elaboration::ImplExprAtom<'tcx>, state: S as s)]
64#[derive(Clone, Debug, Hash, PartialEq, Eq)]
65pub enum ImplExprAtom {
66    /// A concrete `impl Trait for Type {}` item.
67    Concrete(ItemRef),
68    /// A context-bound clause like `where T: Trait`.
69    LocalBound {
70        id: GenericPredicateId,
71        r#trait: Binder<TraitRef>,
72        path: Vec<ImplExprPathChunk>,
73    },
74    /// The implicit `Self: Trait` clause present inside a `trait Trait {}` item.
75    // TODO: should we also get that clause for trait impls?
76    SelfImpl {
77        r#trait: Binder<TraitRef>,
78        path: Vec<ImplExprPathChunk>,
79    },
80    /// `dyn Trait` is a wrapped value with a virtual table for trait
81    /// `Trait`.  In other words, a value `dyn Trait` is a dependent
82    /// triple that gathers a type τ, a value of type τ and an
83    /// instance of type `Trait`.
84    /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that
85    /// built-in implementation.
86    Dyn,
87    /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This
88    /// morally points to an invisible `impl` block; as such it contains the information we may
89    /// need from one.
90    Builtin {
91        /// Extra data for the given trait.
92        trait_data: BuiltinTraitData,
93        /// The `ImplExpr`s required to satisfy the implied predicates on the trait declaration.
94        /// E.g. since `FnMut: FnOnce`, a built-in `T: FnMut` impl would have an `ImplExpr` for `T:
95        /// FnOnce`.
96        impl_exprs: Vec<ImplExpr>,
97        /// The values of the associated types for this trait.
98        types: Vec<(DefId, Ty, Vec<ImplExpr>)>,
99    },
100    /// An error happened while resolving traits.
101    Error(String),
102}
103
104#[derive(AdtInto)]
105#[args(<'tcx, S: UnderOwnerState<'tcx> >, from: elaboration::BuiltinTraitData<'tcx>, state: S as s)]
106#[derive(Clone, Debug, Hash, PartialEq, Eq)]
107pub enum BuiltinTraitData {
108    /// A virtual `Destruct` implementation.
109    /// `Destruct` is implemented automatically for all types. For our purposes, we chose to attach
110    /// the information about `drop_in_place` to that trait. This data tells us what kind of
111    /// `drop_in_place` the target type has.
112    Destruct(DestructData),
113    /// Some other builtin trait.
114    Other,
115}
116
117#[derive(AdtInto)]
118#[args(<'tcx, S: UnderOwnerState<'tcx> >, from: elaboration::DestructData<'tcx>, state: S as s)]
119#[derive(Clone, Debug, Hash, PartialEq, Eq)]
120pub enum DestructData {
121    /// A drop that does nothing, e.g. for scalars and pointers.
122    Noop,
123    /// An implicit `Destruct` local clause, if the `resolve_destruct_bounds` option is `false`. If
124    /// that option is `true`, we'll add `Destruct` bounds to every type param, and use that to
125    /// resolve `Destruct` impls of generics. If it's `false`, we use this variant to indicate that
126    /// the clause comes from a generic or associated type.
127    Implicit,
128    /// The `drop_in_place` is known and non-trivial.
129    Glue {
130        /// The type we're generating glue for.
131        ty: Ty,
132    },
133}
134
135/// An `ImplExpr` describes the full data of a trait implementation. Because of generics, this may
136/// need to combine several concrete trait implementation items. For example, `((1u8, 2u8),
137/// "hello").clone()` combines the generic implementation of `Clone` for `(A, B)` with the
138/// concrete implementations for `u8` and `&str`, represented as a tree.
139pub type ImplExpr = HashConsed<ImplExprContents>;
140
141#[derive(Clone, Debug, Hash, PartialEq, Eq, AdtInto)]
142#[args(<'tcx, S: UnderOwnerState<'tcx> >, from: elaboration::ImplExpr<'tcx>, state: S as s)]
143pub struct ImplExprContents {
144    /// The trait this is an impl for.
145    pub r#trait: Binder<TraitRef>,
146    /// The kind of implemention of the root of the tree.
147    pub r#impl: ImplExprAtom,
148}
149
150impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ImplExpr> for elaboration::ImplExpr<'tcx> {
151    fn sinto(&self, s: &S) -> ImplExpr {
152        HashConsed::new(self.sinto(s))
153    }
154}
155
156/// Given a clause `clause` in the context of some impl block `impl_did`, susbts correctly `Self`
157/// from `clause` and (1) derive a `Clause` and (2) resolve an `ImplExpr`.
158pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>(
159    s: &S,
160    impl_did: rustc_span::def_id::DefId,
161    clause: rustc_middle::ty::Clause<'tcx>,
162    span: rustc_span::Span,
163) -> Option<(Clause, ImplExpr, Span)> {
164    let tcx = s.base().tcx;
165    if !matches!(
166        tcx.def_kind(impl_did),
167        rustc_hir::def::DefKind::Impl { of_trait: true }
168    ) {
169        return None;
170    }
171    let impl_trait_ref =
172        rustc_middle::ty::Binder::dummy(tcx.impl_trait_ref(impl_did).instantiate_identity());
173    let new_clause = clause.instantiate_supertrait(tcx, impl_trait_ref);
174    let impl_expr = solve_trait(
175        s,
176        new_clause
177            .as_predicate()
178            .as_trait_clause()?
179            .to_poly_trait_ref(),
180    );
181    let new_clause = new_clause.sinto(s);
182    Some((new_clause, impl_expr, span.sinto(s)))
183}
184
185/// This is the entrypoint of the solving.
186#[tracing::instrument(level = "trace", skip(s))]
187pub fn solve_trait<'tcx, S: UnderOwnerState<'tcx>>(
188    s: &S,
189    trait_ref: rustc_middle::ty::PolyTraitRef<'tcx>,
190) -> ImplExpr {
191    if let Some(impl_expr) = s.with_cache(|cache| cache.impl_exprs.get(&trait_ref).cloned()) {
192        return impl_expr;
193    }
194    let impl_expr = s.with_predicate_searcher(|pred_searcher| pred_searcher.resolve(&trait_ref));
195    let impl_expr: ImplExpr = impl_expr.sinto(s);
196    s.with_cache(|cache| cache.impl_exprs.insert(trait_ref, impl_expr.clone()));
197    impl_expr
198}
199
200/// Translate a reference to an item, resolving the appropriate trait clauses as needed.
201#[tracing::instrument(level = "trace", skip(s), ret)]
202pub fn translate_item_ref<'tcx, S: UnderOwnerState<'tcx>>(
203    s: &S,
204    def_id: RDefId,
205    generics: ty::GenericArgsRef<'tcx>,
206) -> ItemRef {
207    ItemRef::translate(s, def_id, generics)
208}
209
210/// Solve the trait obligations for a specific item use (for example, a method call, an ADT, etc.)
211/// in the current context. Just like generic args include generics of parent items, this includes
212/// impl exprs for parent items.
213#[tracing::instrument(level = "trace", skip(s), ret)]
214pub fn solve_item_required_traits<'tcx, S: UnderOwnerState<'tcx>>(
215    s: &S,
216    def_id: RDefId,
217    generics: ty::GenericArgsRef<'tcx>,
218) -> Vec<ImplExpr> {
219    let predicates = ItemPredicates::required_recursively(
220        s.base().tcx,
221        def_id,
222        &s.base().options.bounds_options,
223    );
224    solve_item_traits_inner(s, generics, predicates)
225}
226
227/// Solve the trait obligations for implementing a trait (or for trait associated type bounds) in
228/// the current context.
229#[tracing::instrument(level = "trace", skip(s), ret)]
230pub fn solve_item_implied_traits<'tcx, S: UnderOwnerState<'tcx>>(
231    s: &S,
232    def_id: RDefId,
233    generics: ty::GenericArgsRef<'tcx>,
234) -> Vec<ImplExpr> {
235    let predicates =
236        ItemPredicates::implied(s.base().tcx, def_id, &s.base().options.bounds_options);
237    solve_item_traits_inner(s, generics, predicates)
238}
239
240/// Apply the given generics to the provided clauses and resolve the trait references in the
241/// current context.
242fn solve_item_traits_inner<'tcx, S: UnderOwnerState<'tcx>>(
243    s: &S,
244    generics: ty::GenericArgsRef<'tcx>,
245    predicates: ItemPredicates<'tcx>,
246) -> Vec<ImplExpr> {
247    let tcx = s.base().tcx;
248    let typing_env = s.typing_env();
249    predicates
250        .iter_trait_clauses()
251        // Substitute the item generics
252        .map(|(_, trait_ref)| ty::EarlyBinder::bind(trait_ref).instantiate(tcx, generics))
253        // We unfortunately don't have a way to normalize without erasing regions.
254        .map(|trait_ref| {
255            tcx.try_normalize_erasing_regions(typing_env, trait_ref)
256                .unwrap_or(trait_ref)
257        })
258        // Resolve
259        .map(|trait_ref| solve_trait(s, trait_ref))
260        .collect()
261}
262
263/// Retrieve the `Self: Trait` clause for a trait associated item.
264pub fn self_clause_for_item<'tcx, S: UnderOwnerState<'tcx>>(
265    s: &S,
266    def_id: RDefId,
267    generics: rustc_middle::ty::GenericArgsRef<'tcx>,
268) -> Option<ImplExpr> {
269    let tcx = s.base().tcx;
270
271    let tr_def_id = tcx.trait_of_assoc(def_id)?;
272    // The "self" predicate in the context of the trait.
273    let self_pred = self_predicate(tcx, tr_def_id);
274    // Substitute to be in the context of the current item.
275    let generics = generics.truncate_to(tcx, tcx.generics_of(tr_def_id));
276    let self_pred = ty::EarlyBinder::bind(self_pred).instantiate(tcx, generics);
277
278    // Resolve
279    Some(solve_trait(s, self_pred))
280}
281
282/// Solve the `T: Sized` predicate.
283pub fn solve_sized<'tcx, S: UnderOwnerState<'tcx>>(s: &S, ty: ty::Ty<'tcx>) -> ImplExpr {
284    let tcx = s.base().tcx;
285    let sized_trait = tcx.lang_items().sized_trait().unwrap();
286    let ty = erase_free_regions(tcx, ty);
287    let tref = ty::Binder::dummy(ty::TraitRef::new(tcx, sized_trait, [ty]));
288    solve_trait(s, tref)
289}
290
291/// Solve the `T: Destruct` predicate.
292pub fn solve_destruct<'tcx, S: UnderOwnerState<'tcx>>(s: &S, ty: ty::Ty<'tcx>) -> ImplExpr {
293    let tcx = s.base().tcx;
294    let destruct_trait = tcx.lang_items().destruct_trait().unwrap();
295    let tref = ty::Binder::dummy(ty::TraitRef::new(tcx, destruct_trait, [ty]));
296    solve_trait(s, tref)
297}
charon_driver/hax/traits.rs

charon_driver/hax/
traits.rs
