charon_driver/translate/
translate_predicates.rs

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

charon_driver/translate/
translate_predicates.rs
