charon_driver/translate/
translate_generics.rs

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

charon_driver/translate/
translate_generics.rs
