charon_driver/translate/
translate_generics.rs

1use crate::translate::translate_predicates::PredicateLocation;
2
3use super::translate_ctx::ItemTransCtx;
4use charon_lib::ast::*;
5use charon_lib::common::hash_by_addr::HashByAddr;
6use hax_frontend_exporter as hax;
7use std::collections::HashMap;
8use std::fmt::Debug;
9use std::sync::Arc;
10
11/// A level of binding for type-level variables. Each item has a top-level binding level
12/// corresponding to the parameters and clauses to the items. We may then encounter inner binding
13/// levels in the following cases:
14/// - `for<..>` binders in predicates;
15/// - `fn<..>` function pointer types;
16/// - `dyn Trait` types, represented as `dyn<T: Trait>` (TODO);
17/// - types in a trait declaration or implementation block (TODO);
18/// - methods in a trait declaration or implementation block (TODO).
19///
20/// At each level, we store two things: a `GenericParams` that contains the parameters bound at
21/// this level, and various maps from the rustc-internal indices to our indices.
22#[derive(Debug, Default)]
23pub(crate) struct BindingLevel {
24    /// The parameters and predicates bound at this level.
25    pub params: GenericParams,
26    /// Whether this binder corresponds to an item (method, type) or not (`for<..>` predicate, `fn`
27    /// pointer, etc). This indicates whether it corresponds to a rustc `ParamEnv` and therefore
28    /// whether we should resolve rustc variables there.
29    pub is_item_binder: bool,
30    /// Rust makes the distinction between early and late-bound region parameters. We do not make
31    /// this distinction, and merge early and late bound regions. For details, see:
32    /// <https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/>
33    /// <https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/>
34    ///
35    /// The map from rust early regions to translated region indices.
36    pub early_region_vars: std::collections::BTreeMap<hax::EarlyParamRegion, RegionId>,
37    /// The map from rust late/bound regions to translated region indices.
38    pub bound_region_vars: Vec<RegionId>,
39    /// The regions added for by-ref upvars, in order of upvars.
40    pub by_ref_upvar_regions: Vec<RegionId>,
41    /// The map from rust type variable indices to translated type variable indices.
42    pub type_vars_map: HashMap<u32, TypeVarId>,
43    /// The map from rust const generic variables to translate const generic variable indices.
44    pub const_generic_vars_map: HashMap<u32, ConstGenericVarId>,
45    /// Cache the translation of types. This harnesses the deduplication of `TyKind` that hax does.
46    // Important: we can't reuse type caches from earlier binders as the new binder may change what
47    // a given variable resolves to.
48    pub type_trans_cache: HashMap<HashByAddr<Arc<hax::TyKind>>, Ty>,
49}
50
51/// Small helper: we ignore some region names (when they are equal to "'_")
52fn translate_region_name(s: String) -> Option<String> {
53    if s == "'_" {
54        None
55    } else {
56        Some(s)
57    }
58}
59
60impl BindingLevel {
61    pub(crate) fn new(is_item_binder: bool) -> Self {
62        Self {
63            is_item_binder,
64            ..Default::default()
65        }
66    }
67
68    /// Important: we must push all the early-bound regions before pushing any other region.
69    pub(crate) fn push_early_region(&mut self, region: hax::EarlyParamRegion) -> RegionId {
70        let name = translate_region_name(region.name.clone());
71        // Check that there are no late-bound regions
72        assert!(
73            self.bound_region_vars.is_empty(),
74            "Early regions must be translated before late ones"
75        );
76        let rid = self
77            .params
78            .regions
79            .push_with(|index| RegionVar { index, name });
80        self.early_region_vars.insert(region, rid);
81        rid
82    }
83
84    /// Important: we must push all the early-bound regions before pushing any other region.
85    pub(crate) fn push_bound_region(&mut self, region: hax::BoundRegionKind) -> RegionId {
86        use hax::BoundRegionKind::*;
87        let name = match region {
88            Anon => None,
89            Named(_, symbol) => translate_region_name(symbol.clone()),
90            ClosureEnv => Some("@env".to_owned()),
91        };
92        let rid = self
93            .params
94            .regions
95            .push_with(|index| RegionVar { index, name });
96        self.bound_region_vars.push(rid);
97        rid
98    }
99
100    /// Add a region for a by_ref upvar in a closure.
101    pub fn push_upvar_region(&mut self) -> RegionId {
102        // We musn't push to `bound_region_vars` because that will contain the higher-kinded
103        // signature lifetimes if any and they must be lookup-able.
104        let region_id = self
105            .params
106            .regions
107            .push_with(|index| RegionVar { index, name: None });
108        self.by_ref_upvar_regions.push(region_id);
109        region_id
110    }
111
112    pub(crate) fn push_type_var(&mut self, rid: u32, name: String) -> TypeVarId {
113        let var_id = self.params.types.push_with(|index| TypeVar { index, name });
114        self.type_vars_map.insert(rid, var_id);
115        var_id
116    }
117
118    pub(crate) fn push_const_generic_var(&mut self, rid: u32, ty: LiteralTy, name: String) {
119        let var_id = self
120            .params
121            .const_generics
122            .push_with(|index| ConstGenericVar { index, name, ty });
123        self.const_generic_vars_map.insert(rid, var_id);
124    }
125
126    /// Translate a binder of regions by appending the stored reguions to the given vector.
127    pub(crate) fn push_params_from_binder(&mut self, binder: hax::Binder<()>) -> Result<(), Error> {
128        assert!(
129            self.bound_region_vars.is_empty(),
130            "Trying to use two binders at the same binding level"
131        );
132        use hax::BoundVariableKind::*;
133        for p in binder.bound_vars {
134            match p {
135                Region(region) => {
136                    self.push_bound_region(region);
137                }
138                Ty(_) => {
139                    panic!("Unexpected locally bound type variable");
140                }
141                Const => {
142                    panic!("Unexpected locally bound const generic variable");
143                }
144            }
145        }
146        Ok(())
147    }
148}
149
150impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
151    /// Get the only binding level. Panics if there are other binding levels.
152    pub(crate) fn the_only_binder(&self) -> &BindingLevel {
153        assert_eq!(self.binding_levels.len(), 1);
154        self.innermost_binder()
155    }
156
157    /// Get the only binding level. Panics if there are other binding levels.
158    pub(crate) fn the_only_binder_mut(&mut self) -> &mut BindingLevel {
159        assert_eq!(self.binding_levels.len(), 1);
160        self.innermost_binder_mut()
161    }
162
163    pub(crate) fn outermost_binder(&self) -> &BindingLevel {
164        self.binding_levels.outermost()
165    }
166
167    pub(crate) fn innermost_binder(&self) -> &BindingLevel {
168        self.binding_levels.innermost()
169    }
170
171    pub(crate) fn innermost_binder_mut(&mut self) -> &mut BindingLevel {
172        self.binding_levels.innermost_mut()
173    }
174
175    pub(crate) fn innermost_generics_mut(&mut self) -> &mut GenericParams {
176        &mut self.innermost_binder_mut().params
177    }
178
179    pub(crate) fn lookup_bound_region(
180        &mut self,
181        span: Span,
182        dbid: hax::DebruijnIndex,
183        var: hax::BoundVar,
184    ) -> Result<RegionDbVar, Error> {
185        let dbid = DeBruijnId::new(dbid);
186        if let Some(rid) = self
187            .binding_levels
188            .get(dbid)
189            .and_then(|bl| bl.bound_region_vars.get(var))
190        {
191            Ok(DeBruijnVar::bound(dbid, *rid))
192        } else {
193            raise_error!(
194                self,
195                span,
196                "Unexpected error: could not find region '{dbid}_{var}"
197            )
198        }
199    }
200
201    pub(crate) fn lookup_param<Id: Copy>(
202        &mut self,
203        span: Span,
204        f: impl for<'a> Fn(&'a BindingLevel) -> Option<Id>,
205        mk_err: impl FnOnce() -> String,
206    ) -> Result<DeBruijnVar<Id>, Error> {
207        for (dbid, bl) in self.binding_levels.iter_enumerated() {
208            if let Some(id) = f(bl) {
209                return Ok(DeBruijnVar::bound(dbid, id));
210            }
211        }
212        let err = mk_err();
213        raise_error!(self, span, "Unexpected error: could not find {}", err)
214    }
215
216    pub(crate) fn lookup_early_region(
217        &mut self,
218        span: Span,
219        region: &hax::EarlyParamRegion,
220    ) -> Result<RegionDbVar, Error> {
221        self.lookup_param(
222            span,
223            |bl| bl.early_region_vars.get(region).copied(),
224            || format!("the region variable {region:?}"),
225        )
226    }
227
228    pub(crate) fn lookup_type_var(
229        &mut self,
230        span: Span,
231        param: &hax::ParamTy,
232    ) -> Result<TypeDbVar, Error> {
233        self.lookup_param(
234            span,
235            |bl| bl.type_vars_map.get(&param.index).copied(),
236            || format!("the type variable {}", param.name),
237        )
238    }
239
240    pub(crate) fn lookup_const_generic_var(
241        &mut self,
242        span: Span,
243        param: &hax::ParamConst,
244    ) -> Result<ConstGenericDbVar, Error> {
245        self.lookup_param(
246            span,
247            |bl| bl.const_generic_vars_map.get(&param.index).copied(),
248            || format!("the const generic variable {}", param.name),
249        )
250    }
251
252    pub(crate) fn lookup_clause_var(
253        &mut self,
254        span: Span,
255        mut id: usize,
256    ) -> Result<ClauseDbVar, Error> {
257        if self.self_clause_id.is_some() {
258            // We added an extra first clause which hax doesn't know about, so we adapt the index
259            // accordingly.
260            // TODO: more robust tracking of clause ids between hax and charon.
261            id += 1;
262        }
263        // The clause indices returned by hax count clauses in order, starting from the parentmost.
264        // While adding clauses to a binding level we already need to translate types and clauses,
265        // so the innermost item binder may not have all the clauses yet. Hence for that binder we
266        // ignore the clause count.
267        let innermost_item_binder_id = self
268            .binding_levels
269            .iter_enumerated()
270            .find(|(_, bl)| bl.is_item_binder)
271            .unwrap()
272            .0;
273        // Iterate over the binders, starting from the outermost.
274        for (dbid, bl) in self.binding_levels.iter_enumerated().rev() {
275            let num_clauses_bound_at_this_level = bl.params.trait_clauses.elem_count();
276            if id < num_clauses_bound_at_this_level || dbid == innermost_item_binder_id {
277                let id = TraitClauseId::from_usize(id);
278                return Ok(DeBruijnVar::bound(dbid, id));
279            } else {
280                id -= num_clauses_bound_at_this_level
281            }
282        }
283        // Actually unreachable
284        raise_error!(
285            self,
286            span,
287            "Unexpected error: could not find clause variable {}",
288            id
289        )
290    }
291
292    pub(crate) fn push_generic_params(&mut self, generics: &hax::TyGenerics) -> Result<(), Error> {
293        for param in &generics.params {
294            self.push_generic_param(param)?;
295        }
296        Ok(())
297    }
298
299    pub(crate) fn push_generic_param(&mut self, param: &hax::GenericParamDef) -> Result<(), Error> {
300        match &param.kind {
301            hax::GenericParamDefKind::Lifetime => {
302                let region = hax::EarlyParamRegion {
303                    index: param.index,
304                    name: param.name.clone(),
305                };
306                let _ = self.innermost_binder_mut().push_early_region(region);
307            }
308            hax::GenericParamDefKind::Type { .. } => {
309                let _ = self
310                    .innermost_binder_mut()
311                    .push_type_var(param.index, param.name.clone());
312            }
313            hax::GenericParamDefKind::Const { ty, .. } => {
314                let span = self.def_span(&param.def_id);
315                // The type should be primitive, meaning it shouldn't contain variables,
316                // non-primitive adts, etc. As a result, we can use an empty context.
317                let ty = self.translate_ty(span, ty)?;
318                match ty.kind().as_literal() {
319                    Some(ty) => self.innermost_binder_mut().push_const_generic_var(
320                        param.index,
321                        *ty,
322                        param.name.clone(),
323                    ),
324                    None => raise_error!(
325                        self,
326                        span,
327                        "Constant parameters of non-literal type are not supported"
328                    ),
329                }
330            }
331        }
332
333        Ok(())
334    }
335
336    /// Add the generics and predicates of this item and its parents to the current context.
337    #[tracing::instrument(skip(self, span))]
338    fn push_generics_for_def(
339        &mut self,
340        span: Span,
341        def: &hax::FullDef,
342        is_parent: bool,
343        explicit_self_clause: bool,
344    ) -> Result<(), Error> {
345        use hax::FullDefKind::*;
346        // Add generics from the parent item, recursively (recursivity is important for closures,
347        // as they can be nested).
348        match def.kind() {
349            AssocTy { .. }
350            | AssocFn { .. }
351            | AssocConst { .. }
352            | AnonConst { .. }
353            | InlineConst { .. }
354            | PromotedConst { .. }
355            | Closure { .. }
356            | Ctor { .. }
357            | Variant { .. } => {
358                let parent_def_id = def.parent.as_ref().unwrap();
359                let parent_def = self.hax_def(parent_def_id)?;
360                self.push_generics_for_def(span, &parent_def, true, true)?;
361            }
362            _ => {}
363        }
364        self.push_generics_for_def_without_parents(
365            span,
366            def,
367            !is_parent,
368            !is_parent,
369            explicit_self_clause,
370        )?;
371        Ok(())
372    }
373
374    /// Add the generics and predicates of this item. This does not include the parent generics;
375    /// use `push_generics_for_def` to get the full list.
376    fn push_generics_for_def_without_parents(
377        &mut self,
378        span: Span,
379        def: &hax::FullDef,
380        include_late_bound: bool,
381        include_assoc_ty_clauses: bool,
382        explicit_self_clause: bool,
383    ) -> Result<(), Error> {
384        use hax::FullDefKind;
385        if let Some(param_env) = def.param_env() {
386            // Add the generic params.
387            self.push_generic_params(&param_env.generics)?;
388            // Add the explicit self trait clause if required.
389            if let FullDefKind::Trait { self_predicate, .. } = &def.kind
390                && explicit_self_clause
391            {
392                // We add an explicit `Self` clause to trait method declarations. Trait method
393                // implementations already don't use the implicit `Self` clause. This way, methods
394                // don't need an implicit `Self` clause: they're normal functions, and the trait
395                // decl/impl takes care to pass the right arguments.
396                let self_predicate =
397                    RegionBinder::empty(self.translate_trait_predicate(span, self_predicate)?);
398                let clause_id =
399                    self.innermost_generics_mut()
400                        .trait_clauses
401                        .push_with(|clause_id| TraitClause {
402                            clause_id,
403                            origin: PredicateOrigin::TraitSelf,
404                            span: Some(span),
405                            trait_: self_predicate,
406                        });
407                // Record the id so we can resolve `ImplExpr::Self`s to it.
408                self.self_clause_id = Some(clause_id);
409            }
410            // Add the predicates.
411            let origin = match &def.kind {
412                FullDefKind::Struct { .. }
413                | FullDefKind::Union { .. }
414                | FullDefKind::Enum { .. }
415                | FullDefKind::TyAlias { .. }
416                | FullDefKind::AssocTy { .. } => PredicateOrigin::WhereClauseOnType,
417                FullDefKind::Fn { .. }
418                | FullDefKind::AssocFn { .. }
419                | FullDefKind::Const { .. }
420                | FullDefKind::AssocConst { .. }
421                | FullDefKind::AnonConst { .. }
422                | FullDefKind::InlineConst { .. }
423                | FullDefKind::PromotedConst { .. }
424                | FullDefKind::Static { .. } => PredicateOrigin::WhereClauseOnFn,
425                FullDefKind::TraitImpl { .. } | FullDefKind::InherentImpl { .. } => {
426                    PredicateOrigin::WhereClauseOnImpl
427                }
428                FullDefKind::Trait { .. } | FullDefKind::TraitAlias { .. } => {
429                    let _ = self.register_trait_decl_id(span, &def.def_id);
430                    PredicateOrigin::WhereClauseOnTrait
431                }
432                _ => panic!("Unexpected def: {def:?}"),
433            };
434            self.register_predicates(
435                &param_env.predicates,
436                origin.clone(),
437                &PredicateLocation::Base,
438            )?;
439            // Also register implied predicates.
440            if let FullDefKind::Trait {
441                implied_predicates, ..
442            }
443            | FullDefKind::TraitAlias {
444                implied_predicates, ..
445            }
446            | FullDefKind::AssocTy {
447                implied_predicates, ..
448            } = &def.kind
449            {
450                self.register_predicates(implied_predicates, origin, &PredicateLocation::Parent)?;
451            }
452
453            if let hax::FullDefKind::Trait { items, .. } = &def.kind
454                && include_assoc_ty_clauses
455            {
456                // Also add the predicates on associated types.
457                // FIXME(gat): don't skip GATs.
458                // FIXME: don't mix up implied and required predicates.
459                for (_item, item_def) in items {
460                    if let hax::FullDefKind::AssocTy {
461                        param_env,
462                        implied_predicates,
463                        ..
464                    } = &item_def.kind
465                        && param_env.generics.params.is_empty()
466                    {
467                        let name = self.t_ctx.translate_trait_item_name(item_def.def_id())?;
468                        self.register_predicates(
469                            &implied_predicates,
470                            PredicateOrigin::TraitItem(name.clone()),
471                            &PredicateLocation::Item(name),
472                        )?;
473                    }
474                }
475            }
476        }
477
478        if let hax::FullDefKind::Closure { args, .. } = def.kind()
479            && include_late_bound
480        {
481            // Add the lifetime generics coming from the by-ref upvars.
482            args.upvar_tys.iter().for_each(|ty| {
483                if matches!(
484                    ty.kind(),
485                    hax::TyKind::Ref(
486                        hax::Region {
487                            kind: hax::RegionKind::ReErased
488                        },
489                        ..
490                    )
491                ) {
492                    self.the_only_binder_mut().push_upvar_region();
493                }
494            });
495        }
496
497        // The parameters (and in particular the lifetimes) are split between
498        // early bound and late bound parameters. See those blog posts for explanations:
499        // https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/
500        // https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/
501        // Note that only lifetimes can be late bound.
502        //
503        // [TyCtxt.generics_of] gives us the early-bound parameters. We add the late-bound
504        // parameters here.
505        let signature = match &def.kind {
506            hax::FullDefKind::Fn { sig, .. } => Some(sig),
507            hax::FullDefKind::AssocFn { sig, .. } => Some(sig),
508            _ => None,
509        };
510        if let Some(signature) = signature
511            && include_late_bound
512        {
513            let innermost_binder = self.innermost_binder_mut();
514            assert!(innermost_binder.bound_region_vars.is_empty());
515            innermost_binder.push_params_from_binder(signature.rebind(()))?;
516        }
517
518        Ok(())
519    }
520
521    /// Translate the generics and predicates of this item and its parents.
522    pub(crate) fn translate_def_generics(
523        &mut self,
524        span: Span,
525        def: &hax::FullDef,
526    ) -> Result<(), Error> {
527        assert!(self.binding_levels.len() == 0);
528        self.binding_levels.push(BindingLevel::new(true));
529        self.push_generics_for_def(span, def, false, false)?;
530        self.innermost_binder_mut().params.check_consistency();
531        Ok(())
532    }
533
534    /// Translate the generics and predicates of this item without its parents.
535    pub(crate) fn translate_def_generics_without_parents(
536        &mut self,
537        span: Span,
538        def: &hax::FullDef,
539    ) -> Result<(), Error> {
540        self.binding_levels.push(BindingLevel::new(true));
541        self.push_generics_for_def_without_parents(span, def, true, true, false)?;
542        self.innermost_binder().params.check_consistency();
543        Ok(())
544    }
545
546    /// Push a new binding level corresponding to the provided `def` for the duration of the inner
547    /// function call.
548    pub(crate) fn translate_binder_for_def<F, U>(
549        &mut self,
550        span: Span,
551        kind: BinderKind,
552        def: &hax::FullDef,
553        f: F,
554    ) -> Result<Binder<U>, Error>
555    where
556        F: FnOnce(&mut Self) -> Result<U, Error>,
557    {
558        assert!(!self.binding_levels.is_empty());
559
560        // Register the type-level parameters. This pushes a new binding level.
561        self.translate_def_generics_without_parents(span, def)?;
562
563        // Call the continuation. Important: do not short-circuit on error here.
564        let res = f(self);
565
566        // Reset
567        let params = self.binding_levels.pop().unwrap().params;
568
569        // Return
570        res.map(|skip_binder| Binder {
571            kind,
572            params,
573            skip_binder,
574        })
575    }
576
577    /// Push a group of bound regions and call the continuation.
578    /// We use this when diving into a `for<'a>`, or inside an arrow type (because
579    /// it contains universally quantified regions).
580    pub(crate) fn translate_region_binder<F, T, U>(
581        &mut self,
582        _span: Span,
583        binder: &hax::Binder<T>,
584        f: F,
585    ) -> Result<RegionBinder<U>, Error>
586    where
587        F: FnOnce(&mut Self, &T) -> Result<U, Error>,
588    {
589        assert!(!self.binding_levels.is_empty());
590
591        // Register the variables
592        let mut binding_level = BindingLevel::new(false);
593        binding_level.push_params_from_binder(binder.rebind(()))?;
594        self.binding_levels.push(binding_level);
595
596        // Call the continuation. Important: do not short-circuit on error here.
597        let res = f(self, binder.hax_skip_binder_ref());
598
599        // Reset
600        let regions = self.binding_levels.pop().unwrap().params.regions;
601
602        // Return
603        res.map(|skip_binder| RegionBinder {
604            regions,
605            skip_binder,
606        })
607    }
608
609    pub(crate) fn into_generics(mut self) -> GenericParams {
610        assert!(self.binding_levels.len() == 1);
611        self.binding_levels.pop().unwrap().params
612    }
613}
charon_driver/translate/translate_generics.rs

charon_driver/translate/
translate_generics.rs
