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

charon_driver/hax/
traits.rs
