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.t_ctx.hax_def(parent_def_id)?;
360                // Add an explicit `Self` clause to trait item declarations.
361                let explicit_self_clause = matches!(parent_def.kind(), Trait { .. });
362                self.push_generics_for_def(span, &parent_def, true, explicit_self_clause)?;
363            }
364            _ => {}
365        }
366        self.push_generics_for_def_without_parents(
367            span,
368            def,
369            !is_parent,
370            !is_parent,
371            explicit_self_clause,
372        )?;
373        Ok(())
374    }
375
376    /// Add the generics and predicates of this item. This does not include the parent generics;
377    /// use `push_generics_for_def` to get the full list.
378    fn push_generics_for_def_without_parents(
379        &mut self,
380        span: Span,
381        def: &hax::FullDef,
382        include_late_bound: bool,
383        include_assoc_ty_clauses: bool,
384        explicit_self_clause: bool,
385    ) -> Result<(), Error> {
386        use hax::FullDefKind;
387        if let Some(param_env) = def.param_env() {
388            // Add the generic params.
389            self.push_generic_params(&param_env.generics)?;
390            // Add the explicit self trait clause if required.
391            if let FullDefKind::Trait { self_predicate, .. } = &def.kind
392                && explicit_self_clause
393            {
394                // We add an explicit `Self` clause to trait method declarations. Trait method
395                // implementations already don't use the implicit `Self` clause. This way, methods
396                // don't need an implicit `Self` clause: they're normal functions, and the trait
397                // decl/impl takes care to pass the right arguments.
398                let self_predicate =
399                    RegionBinder::empty(self.translate_trait_predicate(span, self_predicate)?);
400                let clause_id =
401                    self.innermost_generics_mut()
402                        .trait_clauses
403                        .push_with(|clause_id| TraitClause {
404                            clause_id,
405                            origin: PredicateOrigin::TraitSelf,
406                            span: Some(span),
407                            trait_: self_predicate,
408                        });
409                // Record the id so we can resolve `ImplExpr::Self`s to it.
410                self.self_clause_id = Some(clause_id);
411            }
412            // Add the predicates.
413            let origin = match &def.kind {
414                FullDefKind::Struct { .. }
415                | FullDefKind::Union { .. }
416                | FullDefKind::Enum { .. }
417                | FullDefKind::TyAlias { .. }
418                | FullDefKind::AssocTy { .. } => PredicateOrigin::WhereClauseOnType,
419                FullDefKind::Fn { .. }
420                | FullDefKind::AssocFn { .. }
421                | FullDefKind::Const { .. }
422                | FullDefKind::AssocConst { .. }
423                | FullDefKind::AnonConst { .. }
424                | FullDefKind::InlineConst { .. }
425                | FullDefKind::PromotedConst { .. }
426                | FullDefKind::Static { .. } => PredicateOrigin::WhereClauseOnFn,
427                FullDefKind::TraitImpl { .. } | FullDefKind::InherentImpl { .. } => {
428                    PredicateOrigin::WhereClauseOnImpl
429                }
430                FullDefKind::Trait { .. } => {
431                    let _ = self.register_trait_decl_id(span, &def.def_id);
432                    PredicateOrigin::WhereClauseOnTrait
433                }
434                _ => panic!("Unexpected def: {def:?}"),
435            };
436            self.register_predicates(
437                &param_env.predicates,
438                origin.clone(),
439                &PredicateLocation::Base,
440            )?;
441            // Also register implied predicates.
442            if let FullDefKind::Trait {
443                implied_predicates, ..
444            }
445            | FullDefKind::AssocTy {
446                implied_predicates, ..
447            } = &def.kind
448            {
449                self.register_predicates(implied_predicates, origin, &PredicateLocation::Parent)?;
450            }
451
452            if let hax::FullDefKind::Trait { items, .. } = &def.kind
453                && include_assoc_ty_clauses
454            {
455                // Also add the predicates on associated types.
456                // FIXME(gat): don't skip GATs.
457                // FIXME: don't mix up implied and required predicates.
458                for (item, item_def) in items {
459                    if let hax::FullDefKind::AssocTy {
460                        param_env,
461                        implied_predicates,
462                        ..
463                    } = &item_def.kind
464                        && param_env.generics.params.is_empty()
465                    {
466                        let name = TraitItemName(item.name.clone());
467                        self.register_predicates(
468                            &implied_predicates,
469                            PredicateOrigin::TraitItem(name.clone()),
470                            &PredicateLocation::Item(name),
471                        )?;
472                    }
473                }
474            }
475        }
476
477        if let hax::FullDefKind::Closure { args, .. } = def.kind()
478            && include_late_bound
479        {
480            // Add the lifetime generics coming from the by-ref upvars.
481            args.upvar_tys.iter().for_each(|ty| {
482                if matches!(
483                    ty.kind(),
484                    hax::TyKind::Ref(
485                        hax::Region {
486                            kind: hax::RegionKind::ReErased
487                        },
488                        ..
489                    )
490                ) {
491                    self.the_only_binder_mut().push_upvar_region();
492                }
493            });
494        }
495
496        // The parameters (and in particular the lifetimes) are split between
497        // early bound and late bound parameters. See those blog posts for explanations:
498        // https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/
499        // https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/
500        // Note that only lifetimes can be late bound.
501        //
502        // [TyCtxt.generics_of] gives us the early-bound parameters. We add the late-bound
503        // parameters here.
504        let signature = match &def.kind {
505            hax::FullDefKind::Fn { sig, .. } => Some(sig),
506            hax::FullDefKind::AssocFn { sig, .. } => Some(sig),
507            _ => None,
508        };
509        if let Some(signature) = signature
510            && include_late_bound
511        {
512            let innermost_binder = self.innermost_binder_mut();
513            assert!(innermost_binder.bound_region_vars.is_empty());
514            innermost_binder.push_params_from_binder(signature.rebind(()))?;
515        }
516
517        Ok(())
518    }
519
520    /// Translate the generics and predicates of this item and its parents.
521    pub(crate) fn translate_def_generics(
522        &mut self,
523        span: Span,
524        def: &hax::FullDef,
525    ) -> Result<(), Error> {
526        assert!(self.binding_levels.len() == 0);
527        self.binding_levels.push(BindingLevel::new(true));
528        self.push_generics_for_def(span, def, false, false)?;
529        self.innermost_binder_mut().params.check_consistency();
530        Ok(())
531    }
532
533    /// Translate the generics and predicates of this item without its parents.
534    pub(crate) fn translate_def_generics_without_parents(
535        &mut self,
536        span: Span,
537        def: &hax::FullDef,
538    ) -> Result<(), Error> {
539        self.binding_levels.push(BindingLevel::new(true));
540        self.push_generics_for_def_without_parents(span, def, true, true, false)?;
541        self.innermost_binder().params.check_consistency();
542        Ok(())
543    }
544
545    /// Push a new binding level corresponding to the provided `def` for the duration of the inner
546    /// function call.
547    pub(crate) fn translate_binder_for_def<F, U>(
548        &mut self,
549        span: Span,
550        kind: BinderKind,
551        def: &hax::FullDef,
552        f: F,
553    ) -> Result<Binder<U>, Error>
554    where
555        F: FnOnce(&mut Self) -> Result<U, Error>,
556    {
557        assert!(!self.binding_levels.is_empty());
558
559        // Register the type-level parameters. This pushes a new binding level.
560        self.translate_def_generics_without_parents(span, def)?;
561
562        // Call the continuation. Important: do not short-circuit on error here.
563        let res = f(self);
564
565        // Reset
566        let params = self.binding_levels.pop().unwrap().params;
567
568        // Return
569        res.map(|skip_binder| Binder {
570            kind,
571            params,
572            skip_binder,
573        })
574    }
575
576    /// Push a group of bound regions and call the continuation.
577    /// We use this when diving into a `for<'a>`, or inside an arrow type (because
578    /// it contains universally quantified regions).
579    pub(crate) fn translate_region_binder<F, T, U>(
580        &mut self,
581        _span: Span,
582        binder: &hax::Binder<T>,
583        f: F,
584    ) -> Result<RegionBinder<U>, Error>
585    where
586        F: FnOnce(&mut Self, &T) -> Result<U, Error>,
587    {
588        assert!(!self.binding_levels.is_empty());
589
590        // Register the variables
591        let mut binding_level = BindingLevel::new(false);
592        binding_level.push_params_from_binder(binder.rebind(()))?;
593        self.binding_levels.push(binding_level);
594
595        // Call the continuation. Important: do not short-circuit on error here.
596        let res = f(self, binder.hax_skip_binder_ref());
597
598        // Reset
599        let regions = self.binding_levels.pop().unwrap().params.regions;
600
601        // Return
602        res.map(|skip_binder| RegionBinder {
603            regions,
604            skip_binder,
605        })
606    }
607
608    pub(crate) fn into_generics(mut self) -> GenericParams {
609        assert!(self.binding_levels.len() == 1);
610        self.binding_levels.pop().unwrap().params
611    }
612}
charon_driver/translate/translate_generics.rs

charon_driver/translate/
translate_generics.rs
