charon_driver/translate/
translate_generics.rs

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