charon_driver/translate/
translate_predicates.rs

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

charon_driver/translate/
translate_predicates.rs
