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

charon_driver/hax/
traits.rs
