charon_driver/translate/
translate_predicates.rs

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

charon_driver/translate/
translate_predicates.rs
