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

charon_driver/hax/
traits.rs
