charon_driver/translate/
translate_predicates.rs

1use super::translate_ctx::*;
2use charon_lib::ast::*;
3use charon_lib::ids::IndexMap;
4use rustc_span::{kw, sym};
5
6impl<'tcx> TranslateCtx<'tcx> {
7    pub fn recognize_builtin_impl(
8        &self,
9        trait_data: &hax::BuiltinTraitData,
10        trait_def: &hax::FullDef,
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::Other => match &trait_def.lang_item {
22                _ if self
23                    .tcx
24                    .trait_is_auto(trait_def.def_id().real_rust_def_id()) =>
25                {
26                    BuiltinImplData::Auto
27                }
28                None => return None,
29                Some(litem) => match *litem {
30                    sym::sized => BuiltinImplData::Sized,
31                    sym::meta_sized => BuiltinImplData::MetaSized,
32                    sym::tuple_trait => BuiltinImplData::Tuple,
33                    kw::Fn => BuiltinImplData::Fn,
34                    sym::fn_mut => BuiltinImplData::FnMut,
35                    sym::fn_once => BuiltinImplData::FnOnce,
36                    sym::pointee_trait => BuiltinImplData::Pointee,
37                    sym::clone => BuiltinImplData::Clone,
38                    sym::copy => BuiltinImplData::Copy,
39                    sym::discriminant_kind => BuiltinImplData::DiscriminantKind,
40                    _ => return None,
41                },
42            },
43        })
44    }
45}
46
47impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
48    /// Translates the given predicates and stores them as resuired preciates of the innermost
49    /// binder.
50    ///
51    /// This function should be called **after** we translated the generics (type parameters,
52    /// regions...).
53    pub(crate) fn register_predicates(
54        &mut self,
55        preds: &hax::GenericPredicates,
56        origin: PredicateOrigin,
57    ) -> Result<(), Error> {
58        let preds = self.translate_predicates(preds, origin)?;
59        self.innermost_generics_mut().take_predicates_from(preds);
60        Ok(())
61    }
62
63    /// Translates the given predicates. Returns a `GenericParams` that only contains predicates.
64    ///
65    /// This function should be called **after** we translated the generics (type parameters,
66    /// regions...).
67    pub(crate) fn translate_predicates(
68        &mut self,
69        preds: &hax::GenericPredicates,
70        origin: PredicateOrigin,
71    ) -> Result<GenericParams, Error> {
72        let mut out = GenericParams::empty();
73        // Translate the trait predicates first, because associated type constraints may refer to
74        // them. E.g. in `fn foo<I: Iterator<Item=usize>>()`, the `I: Iterator` clause must be
75        // translated before the `<I as Iterator>::Item = usize` predicate.
76        for (clause, span) in &preds.predicates {
77            if matches!(clause.kind.value, hax::ClauseKind::Trait(_)) {
78                self.translate_predicate(clause, span, origin.clone(), &mut out)?;
79            }
80        }
81        for (clause, span) in &preds.predicates {
82            if !matches!(clause.kind.value, hax::ClauseKind::Trait(_)) {
83                self.translate_predicate(clause, span, origin.clone(), &mut out)?;
84            }
85        }
86        Ok(out)
87    }
88
89    pub(crate) fn translate_poly_trait_ref(
90        &mut self,
91        span: Span,
92        bound_trait_ref: &hax::Binder<hax::TraitRef>,
93    ) -> Result<PolyTraitDeclRef, Error> {
94        self.translate_region_binder(span, bound_trait_ref, move |ctx, trait_ref| {
95            ctx.translate_trait_ref(span, trait_ref)
96        })
97    }
98
99    pub(crate) fn translate_poly_trait_predicate(
100        &mut self,
101        span: Span,
102        bound_trait_ref: &hax::Binder<hax::TraitPredicate>,
103    ) -> Result<PolyTraitDeclRef, Error> {
104        self.translate_region_binder(span, bound_trait_ref, move |ctx, trait_ref| {
105            ctx.translate_trait_predicate(span, trait_ref)
106        })
107    }
108
109    pub(crate) fn translate_trait_predicate(
110        &mut self,
111        span: Span,
112        trait_pred: &hax::TraitPredicate,
113    ) -> Result<TraitDeclRef, Error> {
114        // we don't handle negative trait predicates.
115        assert!(trait_pred.is_positive);
116        self.translate_trait_ref(span, &trait_pred.trait_ref)
117    }
118
119    pub(crate) fn translate_trait_ref(
120        &mut self,
121        span: Span,
122        trait_ref: &hax::TraitRef,
123    ) -> Result<TraitDeclRef, Error> {
124        self.translate_trait_decl_ref(span, trait_ref)
125    }
126
127    pub(crate) fn translate_predicate(
128        &mut self,
129        clause: &hax::Clause,
130        hspan: &hax::Span,
131        origin: PredicateOrigin,
132        into: &mut GenericParams,
133    ) -> Result<(), Error> {
134        use hax::ClauseKind;
135        trace!("{:?}", clause);
136        let span = self.translate_span(hspan);
137        match clause.kind.hax_skip_binder_ref() {
138            ClauseKind::Trait(trait_pred) => {
139                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
140                    ctx.translate_trait_predicate(span, trait_pred)
141                })?;
142                into.trait_clauses.push_with(|clause_id| TraitParam {
143                    clause_id,
144                    origin,
145                    span: Some(span),
146                    trait_: pred,
147                });
148            }
149            ClauseKind::RegionOutlives(p) => {
150                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
151                    let r0 = ctx.translate_region(span, &p.lhs)?;
152                    let r1 = ctx.translate_region(span, &p.rhs)?;
153                    Ok(OutlivesPred(r0, r1))
154                })?;
155                into.regions_outlive.push(pred);
156            }
157            ClauseKind::TypeOutlives(p) => {
158                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
159                    let ty = ctx.translate_ty(span, &p.lhs)?;
160                    let r = ctx.translate_region(span, &p.rhs)?;
161                    Ok(OutlivesPred(ty, r))
162                })?;
163                into.types_outlive.push(pred);
164            }
165            ClauseKind::Projection(p) => {
166                // This is used to express constraints over associated types.
167                // For instance:
168                // ```
169                // T : Foo<S = String>
170                //         ^^^^^^^^^^
171                // ```
172                let pred = self.translate_region_binder(span, &clause.kind, |ctx, _| {
173                    let trait_ref = ctx.translate_trait_impl_expr(span, &p.impl_expr)?;
174                    let ty = ctx.translate_ty(span, &p.ty)?;
175                    let type_name = ctx.t_ctx.translate_trait_item_name(&p.assoc_item.def_id)?;
176                    Ok(TraitTypeConstraint {
177                        trait_ref,
178                        type_name,
179                        ty,
180                    })
181                })?;
182                into.trait_type_constraints.push(pred);
183            }
184            ClauseKind::ConstArgHasType(..) => {
185                // These are used for trait resolution to get access to the type of const generics.
186                // We don't need them.
187            }
188            ClauseKind::HostEffect(..) => {
189                // These are used for `const Trait` clauses. Part of the `const_traits` unstable
190                // features. We ignore them for now.
191            }
192            ClauseKind::WellFormed(..) | ClauseKind::ConstEvaluatable(..) => {
193                // This is e.g. a clause `[(); N+1]:` (without anything after the `:`). This is
194                // used to require that the fallible `N+1` expression succeeds, so that it can be
195                // used at the type level. Part of the `generic_const_exprs` unstable feature.
196            }
197            ClauseKind::UnstableFeature(..) => {
198                // Unclear what this means, related to stability markers which we don't care about.
199            }
200            #[expect(unreachable_patterns)]
201            kind => raise_error!(self, span, "Unsupported clause: {:?}", kind),
202        }
203        Ok(())
204    }
205
206    pub(crate) fn translate_trait_impl_exprs(
207        &mut self,
208        span: Span,
209        impl_sources: &[hax::ImplExpr],
210    ) -> Result<IndexMap<TraitClauseId, TraitRef>, Error> {
211        impl_sources
212            .iter()
213            .map(|x| self.translate_trait_impl_expr(span, x))
214            .try_collect()
215    }
216
217    #[tracing::instrument(skip(self, span, impl_expr))]
218    pub(crate) fn translate_trait_impl_expr(
219        &mut self,
220        span: Span,
221        impl_expr: &hax::ImplExpr,
222    ) -> Result<TraitRef, Error> {
223        let trait_decl_ref = self.translate_poly_trait_ref(span, &impl_expr.r#trait)?;
224
225        match self.translate_trait_impl_expr_aux(span, impl_expr, trait_decl_ref.clone()) {
226            Ok(res) => Ok(res),
227            Err(err) => {
228                register_error!(self, span, "Error during trait resolution: {}", &err.msg);
229                Ok(TraitRef::new(
230                    TraitRefKind::Unknown(err.msg),
231                    trait_decl_ref,
232                ))
233            }
234        }
235    }
236
237    pub(crate) fn translate_trait_impl_expr_aux(
238        &mut self,
239        span: Span,
240        impl_source: &hax::ImplExpr,
241        trait_decl_ref: PolyTraitDeclRef,
242    ) -> Result<TraitRef, Error> {
243        trace!("impl_expr: {:#?}", impl_source);
244        use hax::DestructData;
245        use hax::ImplExprAtom;
246
247        let trait_ref = match &impl_source.r#impl {
248            ImplExprAtom::Concrete(item) => {
249                let impl_ref =
250                    self.translate_trait_impl_ref(span, item, TraitImplSource::Normal)?;
251                TraitRef::new(TraitRefKind::TraitImpl(impl_ref), trait_decl_ref)
252            }
253            ImplExprAtom::SelfImpl {
254                r#trait: trait_ref,
255                path,
256            }
257            | ImplExprAtom::LocalBound {
258                r#trait: trait_ref,
259                path,
260                ..
261            } => {
262                trace!(
263                    "impl source (self or clause): param:\n- trait_ref: {:?}\n- path: {:?}",
264                    trait_ref, path,
265                );
266                // If we are refering to a trait clause, we need to find the relevant one.
267                let mut tref_kind = match &impl_source.r#impl {
268                    ImplExprAtom::SelfImpl { .. } => TraitRefKind::SelfId,
269                    ImplExprAtom::LocalBound { index, .. } => {
270                        match self.lookup_clause_var(span, *index) {
271                            Ok(var) => TraitRefKind::Clause(var),
272                            Err(err) => TraitRefKind::Unknown(err.msg),
273                        }
274                    }
275                    _ => unreachable!(),
276                };
277
278                let mut current_pred = self.translate_poly_trait_ref(span, trait_ref)?;
279
280                // Apply the path
281                for path_elem in path {
282                    use hax::ImplExprPathChunk::*;
283                    let trait_ref = Box::new(TraitRef::new(tref_kind, current_pred));
284                    match path_elem {
285                        AssocItem {
286                            item,
287                            predicate,
288                            index,
289                            ..
290                        } => {
291                            let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
292                            tref_kind = TraitRefKind::ItemClause(
293                                trait_ref,
294                                name,
295                                TraitClauseId::new(*index),
296                            );
297                            current_pred = self.translate_poly_trait_predicate(span, predicate)?;
298                        }
299                        Parent {
300                            predicate, index, ..
301                        } => {
302                            tref_kind =
303                                TraitRefKind::ParentClause(trait_ref, TraitClauseId::new(*index));
304                            current_pred = self.translate_poly_trait_predicate(span, predicate)?;
305                        }
306                    }
307                }
308
309                TraitRef::new(tref_kind, trait_decl_ref)
310            }
311            ImplExprAtom::Dyn => TraitRef::new(TraitRefKind::Dyn, trait_decl_ref),
312            ImplExprAtom::Builtin {
313                trait_data,
314                impl_exprs,
315                types,
316                ..
317            } => {
318                let tref = &impl_source.r#trait;
319                let trait_def =
320                    self.hax_def(&tref.hax_skip_binder_ref().erase(self.hax_state_with_id()))?;
321                let kind = if let hax::FullDefKind::TraitAlias { .. } = trait_def.kind() {
322                    // We reuse the same `def_id` to generate a blanket impl for the trait.
323                    let impl_id = self.register_item(
324                        span,
325                        tref.hax_skip_binder_ref(),
326                        TransItemSourceKind::TraitImpl(TraitImplSource::TraitAlias),
327                    );
328                    let mut generics = self.erase_region_binder(trait_decl_ref.clone()).generics;
329                    assert!(
330                        generics.trait_refs.is_empty(),
331                        "found trait alias with non-empty required predicates"
332                    );
333                    generics.trait_refs = self.translate_trait_impl_exprs(span, &impl_exprs)?;
334                    TraitRefKind::TraitImpl(TraitImplRef {
335                        id: impl_id,
336                        generics,
337                    })
338                } else if let hax::BuiltinTraitData::Destruct(DestructData::Glue { ty, .. }) =
339                    trait_data
340                {
341                    let (hax::TyKind::Adt(item)
342                    | hax::TyKind::Closure(hax::ClosureArgs { item, .. })
343                    | hax::TyKind::Array(item)
344                    | hax::TyKind::Slice(item)
345                    | hax::TyKind::Tuple(item)) = ty.kind()
346                    else {
347                        raise_error!(self, span, "failed to translate drop glue for type {ty:?}")
348                    };
349                    TraitRefKind::TraitImpl(self.translate_trait_impl_ref(
350                        span,
351                        item,
352                        TraitImplSource::ImplicitDestruct,
353                    )?)
354                } else {
355                    let Some(builtin_data) = self.recognize_builtin_impl(trait_data, &trait_def)
356                    else {
357                        raise_error!(
358                            self,
359                            span,
360                            "found a built-in trait impl we did not recognize: \
361                            {:?} (lang_item={:?})",
362                            trait_def.def_id(),
363                            trait_def.lang_item,
364                        )
365                    };
366                    // TODO: here, if closure_ty is a FnDef, we need to generate the matching trait
367                    // impls, with an empty state as the first argument.
368                    if let Some(closure_kind) = builtin_data.as_closure_kind()
369                        && let Some(hax::GenericArg::Type(closure_ty)) = impl_source
370                            .r#trait
371                            .hax_skip_binder_ref()
372                            .generic_args
373                            .first()
374                        && let hax::TyKind::Closure(closure_args) = closure_ty.kind()
375                    {
376                        let binder = self.translate_region_binder(
377                            span,
378                            &impl_source.r#trait,
379                            |ctx, _tref| {
380                                ctx.translate_closure_impl_ref(span, closure_args, closure_kind)
381                            },
382                        )?;
383                        TraitRefKind::TraitImpl(self.erase_region_binder(binder))
384                    } else {
385                        let parent_trait_refs =
386                            self.translate_trait_impl_exprs(span, &impl_exprs)?;
387                        let types = if self.monomorphize() {
388                            vec![]
389                        } else {
390                            types
391                                .iter()
392                                .map(|(def_id, ty, impl_exprs)| -> Result<_, Error> {
393                                    let name = self.t_ctx.translate_trait_item_name(def_id)?;
394                                    let assoc_ty = TraitAssocTyImpl {
395                                        value: self.translate_ty(span, ty)?,
396                                        implied_trait_refs: self
397                                            .translate_trait_impl_exprs(span, impl_exprs)?,
398                                    };
399                                    Ok((name, assoc_ty))
400                                })
401                                .try_collect()?
402                        };
403                        TraitRefKind::BuiltinOrAuto {
404                            builtin_data,
405                            parent_trait_refs,
406                            types,
407                        }
408                    }
409                };
410                TraitRef::new(kind, trait_decl_ref)
411            }
412            ImplExprAtom::Error(msg) => {
413                let trait_ref = TraitRef::new(TraitRefKind::Unknown(msg.clone()), trait_decl_ref);
414                if self.error_on_impl_expr_error {
415                    register_error!(self, span, "Error during trait resolution: {}", msg);
416                }
417                trait_ref
418            }
419        };
420        Ok(trait_ref)
421    }
422}
charon_driver/translate/translate_predicates.rs

charon_driver/translate/
translate_predicates.rs
