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

charon_driver/translate/
translate_predicates.rs
