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

charon_driver/hax/
traits.rs
