charon_driver/translate/
translate_predicates.rs

1use super::translate_ctx::*;
2use crate::hax;
3use charon_lib::{ast::*, ids::IndexVec};
4use rustc_type_ir::Interner;
5
6impl<'tcx> TranslateCtx<'tcx> {
7    pub fn recognize_builtin_impl(
8        &self,
9        trait_data: &hax::BuiltinTraitData,
10        trait_def: &hax::FullDef<'tcx>,
11    ) -> Option<BuiltinImplData> {
12        Some(match trait_data {
13            hax::BuiltinTraitData::Destruct(x) => {
14                match x {
15                    hax::DestructData::Noop => BuiltinImplData::NoopDestruct,
16                    hax::DestructData::Implicit => BuiltinImplData::UntrackedDestruct,
17                    // This is unconditionally replaced by a `TraitImpl`.
18                    hax::DestructData::Glue { .. } => return None,
19                }
20            }
21            hax::BuiltinTraitData::Auto => BuiltinImplData::Auto,
22            hax::BuiltinTraitData::Other => {
23                use rustc_type_ir::lang_items::SolverTraitLangItem;
24                // The ones for which we return `None` are those I don't think would show up in a
25                // builtin impl.
26                match self
27                    .tcx
28                    .as_trait_lang_item(trait_def.def_id().real_rust_def_id())?
29                {
30                    SolverTraitLangItem::AsyncFn => BuiltinImplData::AsyncFn,
31                    SolverTraitLangItem::AsyncFnKindHelper => return None,
32                    SolverTraitLangItem::AsyncFnMut => BuiltinImplData::AsyncFnMut,
33                    SolverTraitLangItem::AsyncFnOnce => BuiltinImplData::AsyncFnOnce,
34                    SolverTraitLangItem::AsyncIterator => return None,
35                    SolverTraitLangItem::BikeshedGuaranteedNoDrop => return None,
36                    SolverTraitLangItem::Clone => BuiltinImplData::Clone,
37                    SolverTraitLangItem::Copy => BuiltinImplData::Copy,
38                    SolverTraitLangItem::Coroutine => BuiltinImplData::Coroutine,
39                    SolverTraitLangItem::Destruct => BuiltinImplData::UntrackedDestruct,
40                    SolverTraitLangItem::DiscriminantKind => BuiltinImplData::DiscriminantKind,
41                    SolverTraitLangItem::Drop => return None,
42                    SolverTraitLangItem::Field => return None,
43                    SolverTraitLangItem::Fn => BuiltinImplData::Fn,
44                    SolverTraitLangItem::FnMut => BuiltinImplData::FnMut,
45                    SolverTraitLangItem::FnOnce => BuiltinImplData::FnOnce,
46                    SolverTraitLangItem::FnPtrTrait => BuiltinImplData::FnPtr,
47                    SolverTraitLangItem::FusedIterator => return None,
48                    SolverTraitLangItem::Future => BuiltinImplData::Future,
49                    SolverTraitLangItem::Iterator => return None,
50                    SolverTraitLangItem::MetaSized => BuiltinImplData::MetaSized,
51                    SolverTraitLangItem::PointeeSized => BuiltinImplData::PointeeSized,
52                    SolverTraitLangItem::PointeeTrait => BuiltinImplData::Pointee,
53                    SolverTraitLangItem::Sized => BuiltinImplData::Sized,
54                    SolverTraitLangItem::TransmuteTrait => BuiltinImplData::Transmute,
55                    SolverTraitLangItem::TrivialClone => BuiltinImplData::Auto,
56                    SolverTraitLangItem::TryAsDyn => BuiltinImplData::TryAsDynCompatible,
57                    SolverTraitLangItem::Tuple => BuiltinImplData::Tuple,
58                    SolverTraitLangItem::Unpin => BuiltinImplData::Auto,
59                    SolverTraitLangItem::Unsize => BuiltinImplData::Unsize,
60                }
61            }
62        })
63    }
64}
65
66impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
67    /// Translates the given predicates and stores them as resuired preciates of the innermost
68    /// binder.
69    ///
70    /// This function should be called **after** we translated the generics (type parameters,
71    /// regions...).
72    pub(crate) fn register_predicates(
73        &mut self,
74        preds: &hax::GenericPredicates,
75        origin: PredicateOrigin,
76    ) -> Result<(), Error> {
77        self.translate_predicates(preds, origin, None)?;
78        Ok(())
79    }
80
81    /// Translates the given predicates. This function should be called **after** we translated the
82    /// generics (type parameters, regions...).
83    pub(crate) fn translate_predicates(
84        &mut self,
85        preds: &hax::GenericPredicates,
86        origin: PredicateOrigin,
87        // Either put clauses there or in the innermost binder.
88        mut trait_clauses: Option<&mut IndexVec<TraitClauseId, TraitParam>>,
89    ) -> Result<(), Error> {
90        if trait_clauses.is_none() {
91            // Register the mapping from trait preds to their id early on, as these can be mentioned
92            // while translating any other predicate including themselves. Each trait pred gives rise
93            // to exactly one trait clause inserted into `trait_clauses`, which we use to compute
94            // clause ids.
95            let next_clause_id = self.innermost_generics_mut().trait_clauses.next_idx();
96            for (i, pred) in preds
97                .predicates
98                .iter()
99                .filter(|pred| {
100                    matches!(
101                        pred.clause.kind.hax_skip_binder_ref(),
102                        hax::ClauseKind::Trait(_)
103                    )
104                })
105                .enumerate()
106            {
107                self.innermost_binder_mut()
108                    .trait_preds
109                    .insert(pred.id.clone(), next_clause_id + i);
110            }
111        }
112
113        for pred in &preds.predicates {
114            self.translate_predicate(pred, origin.clone(), trait_clauses.as_deref_mut())?;
115        }
116        Ok(())
117    }
118
119    pub(crate) fn translate_poly_trait_ref(
120        &mut self,
121        span: Span,
122        bound_trait_ref: &hax::Binder<hax::TraitRef>,
123    ) -> Result<PolyTraitDeclRef, Error> {
124        self.translate_region_binder(span, bound_trait_ref, move |ctx, trait_ref| {
125            ctx.translate_trait_ref(span, trait_ref)
126        })
127    }
128
129    pub(crate) fn translate_trait_predicate(
130        &mut self,
131        span: Span,
132        trait_pred: &hax::TraitPredicate,
133    ) -> Result<TraitDeclRef, Error> {
134        // we don't handle negative trait predicates.
135        assert!(trait_pred.is_positive);
136        self.translate_trait_ref(span, &trait_pred.trait_ref)
137    }
138
139    pub(crate) fn translate_trait_ref(
140        &mut self,
141        span: Span,
142        trait_ref: &hax::TraitRef,
143    ) -> Result<TraitDeclRef, Error> {
144        self.translate_trait_decl_ref(span, trait_ref)
145    }
146
147    pub(crate) fn translate_predicate(
148        &mut self,
149        pred: &hax::GenericPredicate,
150        mut origin: PredicateOrigin,
151        // Either put clauses there or in the innermost binder.
152        mut trait_clauses: Option<&mut IndexVec<TraitClauseId, TraitParam>>,
153    ) -> Result<(), Error> {
154        use crate::hax::ClauseKind;
155        let clause = &pred.clause;
156        trace!("{:?}", clause);
157        let span = self.translate_span(&pred.span);
158        match clause.kind.hax_skip_binder_ref() {
159            ClauseKind::Trait(trait_pred) => {
160                if matches!(pred.id, hax::GenericPredicateId::TraitSelf) {
161                    origin = PredicateOrigin::TraitSelf;
162                }
163                let trait_pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
164                    ctx.translate_trait_predicate(span, trait_pred)
165                })?;
166                let clause_id = trait_clauses
167                    .as_deref_mut()
168                    .unwrap_or(&mut self.innermost_generics_mut().trait_clauses)
169                    .push_with(|clause_id| TraitParam {
170                        clause_id,
171                        origin,
172                        span: Some(span),
173                        trait_: trait_pred,
174                    });
175
176                if trait_clauses.is_none() {
177                    // Sanity check.
178                    let expected_clause_id = self
179                        .innermost_binder_mut()
180                        .trait_preds
181                        .get(&pred.id)
182                        .unwrap();
183                    debug_assert_eq!(clause_id, *expected_clause_id);
184                }
185            }
186            ClauseKind::RegionOutlives(p) => {
187                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
188                    let r0 = ctx.translate_region(span, &p.lhs)?;
189                    let r1 = ctx.translate_region(span, &p.rhs)?;
190                    Ok(OutlivesPred(r0, r1))
191                })?;
192                self.innermost_generics_mut().regions_outlive.push(pred);
193            }
194            ClauseKind::TypeOutlives(p) => {
195                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
196                    let ty = ctx.translate_ty(span, &p.lhs)?;
197                    let r = ctx.translate_region(span, &p.rhs)?;
198                    Ok(OutlivesPred(ty, r))
199                })?;
200                self.innermost_generics_mut().types_outlive.push(pred);
201            }
202            ClauseKind::Projection(p) => {
203                // This is used to express constraints over associated types.
204                // For instance:
205                // ```
206                // T : Foo<S = String>
207                //         ^^^^^^^^^^
208                // ```
209                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
210                    let trait_ref = ctx.translate_trait_proof(span, &p.trait_proof)?;
211                    let ty = ctx.translate_ty(span, &p.ty)?;
212                    let type_id =
213                        ctx.translate_assoc_type_id(trait_ref.trait_id(), &p.assoc_item.def_id)?;
214                    Ok(TraitTypeConstraint {
215                        trait_ref,
216                        type_id,
217                        ty,
218                    })
219                })?;
220                self.innermost_generics_mut()
221                    .trait_type_constraints
222                    .push(pred);
223            }
224            ClauseKind::ConstArgHasType(..) => {
225                // These are used for trait resolution to get access to the type of const generics.
226                // We don't need them.
227            }
228            ClauseKind::HostEffect(..) => {
229                // These are used for `const Trait` clauses. Part of the `const_traits` unstable
230                // features. We ignore them for now.
231            }
232            ClauseKind::WellFormed(..) | ClauseKind::ConstEvaluatable(..) => {
233                // This is e.g. a clause `[(); N+1]:` (without anything after the `:`). This is
234                // used to require that the fallible `N+1` expression succeeds, so that it can be
235                // used at the type level. Part of the `generic_const_exprs` unstable feature.
236            }
237            ClauseKind::UnstableFeature(..) => {
238                // Unclear what this means, related to stability markers which we don't care about.
239            }
240            #[expect(unreachable_patterns)]
241            kind => raise_error!(self, span, "Unsupported clause: {:?}", kind),
242        }
243        Ok(())
244    }
245
246    pub(crate) fn translate_trait_proofs(
247        &mut self,
248        span: Span,
249        impl_sources: &[hax::TraitProof],
250    ) -> Result<IndexVec<TraitClauseId, TraitRef>, Error> {
251        impl_sources
252            .iter()
253            .map(|x| self.translate_trait_proof(span, x))
254            .try_collect()
255    }
256
257    #[tracing::instrument(skip(self, span, trait_proof))]
258    pub(crate) fn translate_trait_proof(
259        &mut self,
260        span: Span,
261        trait_proof: &hax::TraitProof,
262    ) -> Result<TraitRef, Error> {
263        let trait_decl_ref = self.translate_poly_trait_ref(span, &trait_proof.pred)?;
264
265        match self.translate_trait_proof_aux(span, trait_proof, trait_decl_ref.clone()) {
266            Ok(res) => Ok(res),
267            Err(err) => {
268                register_error!(self, span, "Error during trait resolution: {}", &err.msg);
269                Ok(TraitRef::new(
270                    TraitRefKind::Unknown(err.msg),
271                    trait_decl_ref,
272                ))
273            }
274        }
275    }
276
277    pub(crate) fn translate_trait_proof_aux(
278        &mut self,
279        span: Span,
280        impl_source: &hax::TraitProof,
281        trait_decl_ref: PolyTraitDeclRef,
282    ) -> Result<TraitRef, Error> {
283        trace!("trait_proof: {:#?}", impl_source);
284        use crate::hax::DestructData;
285        use crate::hax::TraitProofKind;
286
287        let kind = match &impl_source.kind {
288            TraitProofKind::Concrete(item) => {
289                let impl_ref =
290                    self.translate_trait_impl_ref(span, item, TransImplSource::Normal)?;
291                TraitRefKind::TraitImpl(impl_ref)
292            }
293            TraitProofKind::SelfProof => TraitRefKind::SelfId,
294            TraitProofKind::LocalBound(id) => match self.lookup_clause_var(span, id) {
295                Ok(var) => TraitRefKind::Clause(var),
296                Err(err) => TraitRefKind::Unknown(err.msg),
297            },
298            TraitProofKind::Derived {
299                base,
300                path: path_elem,
301            } => {
302                let trait_ref = self.translate_trait_proof(span, base)?;
303                let trait_ref = Box::new(trait_ref);
304                match path_elem {
305                    hax::TraitProofImpliedPredicate::AssocItem { item, index, .. } => {
306                        let assoc_type_id =
307                            self.translate_assoc_type_id(trait_ref.trait_id(), &item.def_id)?;
308                        TraitRefKind::ItemClause(
309                            trait_ref,
310                            assoc_type_id,
311                            TraitClauseId::new(*index),
312                        )
313                    }
314                    hax::TraitProofImpliedPredicate::Parent { index, .. } => {
315                        TraitRefKind::ParentClause(trait_ref, TraitClauseId::new(*index))
316                    }
317                }
318            }
319            TraitProofKind::Dyn => TraitRefKind::Dyn,
320            TraitProofKind::Builtin {
321                trait_data,
322                proofs: trait_proofs,
323                types,
324                ..
325            } => {
326                let tref = &impl_source.pred;
327                let trait_def = self.poly_hax_def(&tref.hax_skip_binder_ref().def_id)?;
328                if let hax::FullDefKind::TraitAlias { .. } = trait_def.kind() {
329                    // We reuse the same `def_id` to generate a blanket impl for the trait.
330                    let mut impl_ref: TraitImplRef = self.translate_item(
331                        span,
332                        &tref.hax_skip_binder_ref().erase(self.hax_state_with_id()),
333                        TransItemSourceKind::TraitImpl(TransImplSource::TraitAlias),
334                    )?;
335                    assert!(
336                        impl_ref.generics.trait_refs.is_empty(),
337                        "found trait alias with non-empty required predicates"
338                    );
339                    impl_ref.generics.trait_refs =
340                        self.translate_trait_proofs(span, trait_proofs)?;
341                    TraitRefKind::TraitImpl(impl_ref)
342                } else if let hax::BuiltinTraitData::Destruct(DestructData::Glue { ty, .. }) =
343                    trait_data
344                {
345                    let (hax::TyKind::Adt(item)
346                    | hax::TyKind::Closure(hax::ClosureArgs { item, .. })
347                    | hax::TyKind::Array(item)
348                    | hax::TyKind::Slice(item)
349                    | hax::TyKind::Tuple(item)) = ty.kind()
350                    else {
351                        raise_error!(self, span, "failed to translate drop glue for type {ty:?}")
352                    };
353                    TraitRefKind::TraitImpl(self.translate_trait_impl_ref(
354                        span,
355                        item,
356                        TransImplSource::ImplicitDestruct,
357                    )?)
358                } else {
359                    let Some(builtin_data) = self.recognize_builtin_impl(trait_data, &trait_def)
360                    else {
361                        raise_error!(
362                            self,
363                            span,
364                            "found a built-in trait impl we did not recognize: \
365                            {:?} (lang_item={:?})",
366                            trait_def.def_id(),
367                            trait_def.lang_item,
368                        )
369                    };
370                    // TODO: here, if closure_ty is a FnDef, we need to generate the matching trait
371                    // impls, with an empty state as the first argument.
372                    if let Some(closure_kind) = builtin_data.as_closure_kind()
373                        && let Some(hax::GenericArg::Type(closure_ty)) =
374                            impl_source.pred.hax_skip_binder_ref().generic_args.first()
375                        && let hax::TyKind::Closure(closure_args) = closure_ty.kind()
376                    {
377                        let binder =
378                            self.translate_region_binder(span, &impl_source.pred, |ctx, _tref| {
379                                ctx.translate_closure_impl_ref(span, closure_args, closure_kind)
380                            })?;
381                        TraitRefKind::TraitImpl(self.erase_region_binder(binder))
382                    } else {
383                        let parent_trait_refs = self.translate_trait_proofs(span, trait_proofs)?;
384                        let types: IndexMap<AssocTypeId, _> = if self.monomorphize() {
385                            IndexMap::new()
386                        } else {
387                            let tdecl_id = trait_decl_ref.skip_binder.id;
388                            let mut type_map = IndexMap::new();
389                            for (def_id, ty, trait_proofs) in types {
390                                let assoc_type_id =
391                                    self.translate_assoc_type_id(tdecl_id, def_id)?;
392                                let assoc_ty = TraitAssocTyImpl {
393                                    value: self.translate_ty(span, ty)?,
394                                    implied_trait_refs: self
395                                        .translate_trait_proofs(span, trait_proofs)?,
396                                };
397                                type_map.set_slot_extend(assoc_type_id, assoc_ty);
398                            }
399                            type_map
400                        };
401                        TraitRefKind::BuiltinOrAuto {
402                            builtin_data,
403                            parent_trait_refs,
404                            types,
405                        }
406                    }
407                }
408            }
409            TraitProofKind::Error(msg) => {
410                if self.error_on_trait_proof_error {
411                    register_error!(self, span, "Error during trait resolution: {}", msg);
412                }
413                TraitRefKind::Unknown(msg.clone())
414            }
415        };
416        Ok(TraitRef::new(kind, trait_decl_ref))
417    }
418}
charon_driver/translate/translate_predicates.rs

charon_driver/translate/
translate_predicates.rs
