charon_driver/translate/
translate_generics.rs

1use std::collections::{HashMap, HashSet};
2use std::fmt::Debug;
3use std::mem;
4
5use crate::hax;
6use crate::hax::{BaseState, Symbol};
7use rustc_middle::ty;
8
9use super::translate_ctx::{ItemTransCtx, TraitImplSource, TransItemSourceKind};
10use charon_lib::ast::*;
11use charon_lib::common::CycleDetector;
12use charon_lib::ids::IndexVec;
13
14/// A level of binding for type-level variables. Each item has a top-level binding level
15/// corresponding to the parameters and clauses to the items. We may then encounter inner binding
16/// levels in the following cases:
17/// - `for<..>` binders in predicates;
18/// - `fn<..>` function pointer types;
19/// - `dyn Trait` types, represented as `dyn<T: Trait>`;
20/// - types in a trait declaration or implementation block;
21/// - methods in a trait declaration or implementation block.
22///
23/// At each level, we store two things: a `GenericParams` that contains the parameters bound at
24/// this level, and various maps from the rustc-internal indices to our indices.
25#[derive(Debug, Default)]
26pub(crate) struct BindingLevel {
27    /// The parameters and predicates bound at this level.
28    pub params: GenericParams,
29    /// Rust makes the distinction between early and late-bound region parameters. We do not make
30    /// this distinction, and merge early and late bound regions. For details, see:
31    /// <https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/>
32    /// <https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/>
33    ///
34    /// The map from rust early regions to translated region indices.
35    pub early_region_vars: HashMap<hax::EarlyParamRegion, RegionId>,
36    /// The map from rust named region parameter ids to translated region indices.
37    pub region_vars_by_def_id: HashMap<hax::DefId, RegionId>,
38    /// The map from rust late/bound regions to translated region indices.
39    pub bound_region_vars: Vec<RegionId>,
40    /// Region added for the lifetime bound in the signature of the `call`/`call_mut` methods.
41    pub closure_call_method_region: Option<RegionId>,
42    /// Region added for the borrow accepted by a drop glue method or vtable drop shim.
43    pub drop_glue_region: Option<RegionId>,
44    /// The map from rust type variable indices to translated type variable indices.
45    pub type_vars_map: HashMap<u32, TypeVarId>,
46    /// The map from rust const generic variables to translated const generic variable indices.
47    pub const_generic_vars_map: HashMap<u32, ConstGenericVarId>,
48    /// The map from trait predicates to translated trait clause indices.
49    pub trait_preds: HashMap<hax::GenericPredicateId, TraitClauseId>,
50    /// The types of the captured variables, when we're translating a closure item. This is
51    /// translated early because this translation requires adding new lifetime generics to the
52    /// current binder.
53    pub closure_upvar_tys: Option<IndexVec<FieldId, Ty>>,
54    /// The regions we added for the upvars.
55    pub closure_upvar_regions: Vec<RegionId>,
56    /// RPITIT can cause region names to be reused. To avoid clashes in our output, we rename
57    /// duplicate names.
58    pub used_region_names: HashSet<Symbol>,
59    /// Cache the translation of types. This harnesses the deduplication of `Ty` that hax does.
60    // Important: we can't reuse type caches from earlier binders as the new binder may change what
61    // a given variable resolves to.
62    pub type_trans_cache: HashMap<hax::Ty, Ty>,
63}
64
65/// Small helper: we ignore some region names (when they are equal to "'_")
66fn translate_region_name(s: hax::Symbol) -> Option<String> {
67    let s = s.to_string();
68    if s == "'_" { None } else { Some(s) }
69}
70
71fn translate_variance(variance: Option<&hax::Variance>) -> Variance {
72    match variance {
73        Some(hax::Variance::Covariant) => Variance::Covariant,
74        Some(hax::Variance::Invariant) => Variance::Invariant,
75        Some(hax::Variance::Contravariant) => Variance::Contravariant,
76        Some(hax::Variance::Bivariant) => Variance::Bivariant,
77        None => Variance::Unknown,
78    }
79}
80
81impl BindingLevel {
82    pub(crate) fn new() -> Self {
83        Self {
84            ..Default::default()
85        }
86    }
87
88    /// Important: we must push all the early-bound regions before pushing any other region.
89    pub(crate) fn push_early_region(
90        &mut self,
91        region: hax::EarlyParamRegion,
92        def_id: hax::DefId,
93        variance: Variance,
94        mutability: LifetimeMutability,
95    ) -> RegionId {
96        let name = if self.used_region_names.insert(region.name) {
97            translate_region_name(region.name)
98        } else {
99            None
100        };
101        // Check that there are no late-bound regions
102        assert!(
103            self.bound_region_vars.is_empty(),
104            "Early regions must be translated before late ones"
105        );
106        let rid = self.params.regions.push_with(|index| RegionParam {
107            index,
108            name,
109            variance,
110            mutability,
111        });
112        self.early_region_vars.insert(region, rid);
113        self.region_vars_by_def_id.insert(def_id, rid);
114        rid
115    }
116
117    /// Important: we must push all the early-bound regions before pushing any other region.
118    pub(crate) fn push_bound_region(
119        &mut self,
120        region: hax::BoundRegionKind,
121        variance: Variance,
122    ) -> RegionId {
123        use crate::hax::BoundRegionKind::*;
124        let (name, def_id) = match region {
125            Anon => (None, None),
126            NamedForPrinting(symbol) => (translate_region_name(symbol), None),
127            Named(def_id, symbol) => (translate_region_name(symbol), Some(def_id)),
128            ClosureEnv => (Some("@env".to_owned()), None),
129        };
130        let rid = self
131            .params
132            .regions
133            .push_with(|index| RegionParam::new(index, name, variance));
134        self.bound_region_vars.push(rid);
135        if let Some(def_id) = def_id {
136            self.region_vars_by_def_id.insert(def_id, rid);
137        }
138        rid
139    }
140
141    /// Add a region for an upvar in a closure.
142    pub fn push_upvar_region(&mut self) -> RegionId {
143        // We musn't push to `bound_region_vars` because that will contain the higher-kinded
144        // signature lifetimes (if any) and they must be lookup-able.
145        let region_id = self
146            .params
147            .regions
148            .push_with(|index| RegionParam::new(index, None, Variance::Unknown));
149        self.closure_upvar_regions.push(region_id);
150        region_id
151    }
152
153    pub fn push_drop_glue_region(&mut self) -> RegionId {
154        let region_id = self
155            .params
156            .regions
157            .push_with(|index| RegionParam::new(index, None, Variance::Covariant));
158        self.drop_glue_region = Some(region_id);
159        region_id
160    }
161
162    pub(crate) fn push_type_var(
163        &mut self,
164        rid: u32,
165        name: hax::Symbol,
166        variance: Variance,
167    ) -> TypeVarId {
168        // Type vars comping from `impl Trait` arguments have as their name the whole `impl Trait`
169        // expression. We turn it into an identifier.
170        let mut name = name.to_string();
171        if name
172            .chars()
173            .any(|c| !(c.is_ascii_alphanumeric() || c == '_'))
174        {
175            name = format!("T{rid}")
176        }
177        let var_id = self.params.types.push_with(|index| TypeParam {
178            index,
179            name,
180            variance,
181        });
182        self.type_vars_map.insert(rid, var_id);
183        var_id
184    }
185
186    pub(crate) fn push_const_generic_var(&mut self, rid: u32, ty: Ty, name: hax::Symbol) {
187        let var_id = self
188            .params
189            .const_generics
190            .push_with(|index| ConstGenericParam {
191                index,
192                name: name.to_string(),
193                ty,
194            });
195        self.const_generic_vars_map.insert(rid, var_id);
196    }
197
198    /// Translate a binder of regions by appending the stored reguions to the given vector.
199    pub(crate) fn push_params_from_binder(&mut self, binder: hax::Binder<()>) -> Result<(), Error> {
200        assert!(
201            self.bound_region_vars.is_empty(),
202            "Trying to use two binders at the same binding level"
203        );
204        use crate::hax::BoundVariableKind::*;
205        for p in binder.bound_vars {
206            match p {
207                Region(region, variance) => {
208                    let variance = translate_variance(variance.as_ref());
209                    self.push_bound_region(region, variance);
210                }
211                Ty(_) => {
212                    panic!("Unexpected locally bound type variable");
213                }
214                Const => {
215                    panic!("Unexpected locally bound const generic variable");
216                }
217            }
218        }
219        Ok(())
220    }
221}
222
223impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
224    /// Get the only binding level. Panics if there are other binding levels.
225    pub(crate) fn the_only_binder(&self) -> &BindingLevel {
226        assert_eq!(self.binding_levels.len(), 1);
227        self.innermost_binder()
228    }
229    /// Get the only binding level. Panics if there are other binding levels.
230    pub(crate) fn the_only_binder_mut(&mut self) -> &mut BindingLevel {
231        assert_eq!(self.binding_levels.len(), 1);
232        self.innermost_binder_mut()
233    }
234
235    pub(crate) fn outermost_binder(&self) -> &BindingLevel {
236        self.binding_levels.outermost()
237    }
238    pub(crate) fn outermost_binder_mut(&mut self) -> &mut BindingLevel {
239        self.binding_levels.outermost_mut()
240    }
241    pub(crate) fn innermost_binder(&self) -> &BindingLevel {
242        self.binding_levels.innermost()
243    }
244    pub(crate) fn innermost_binder_mut(&mut self) -> &mut BindingLevel {
245        self.binding_levels.innermost_mut()
246    }
247
248    pub(crate) fn outermost_generics(&self) -> &GenericParams {
249        &self.outermost_binder().params
250    }
251    #[expect(dead_code)]
252    pub(crate) fn outermost_generics_mut(&mut self) -> &mut GenericParams {
253        &mut self.outermost_binder_mut().params
254    }
255    #[expect(dead_code)]
256    pub(crate) fn innermost_generics(&self) -> &GenericParams {
257        &self.innermost_binder().params
258    }
259    pub(crate) fn innermost_generics_mut(&mut self) -> &mut GenericParams {
260        &mut self.innermost_binder_mut().params
261    }
262
263    pub(crate) fn lookup_bound_region(
264        &mut self,
265        span: Span,
266        dbid: hax::DebruijnIndex,
267        var: hax::BoundVar,
268    ) -> Result<RegionDbVar, Error> {
269        let dbid = DeBruijnId::new(dbid);
270        if let Some(rid) = self
271            .binding_levels
272            .get(dbid)
273            .and_then(|bl| bl.bound_region_vars.get(var))
274        {
275            Ok(DeBruijnVar::bound(dbid, *rid))
276        } else {
277            raise_error!(
278                self,
279                span,
280                "Unexpected error: could not find region '{dbid}_{var}"
281            )
282        }
283    }
284
285    pub(crate) fn lookup_param<Id: Copy>(
286        &mut self,
287        span: Span,
288        f: impl for<'a> Fn(&'a BindingLevel) -> Option<Id>,
289        mk_err: impl FnOnce() -> String,
290    ) -> Result<DeBruijnVar<Id>, Error> {
291        for (dbid, bl) in self.binding_levels.iter_enumerated() {
292            if let Some(id) = f(bl) {
293                return Ok(DeBruijnVar::bound(dbid, id));
294            }
295        }
296        let err = mk_err();
297        raise_error!(self, span, "Unexpected error: could not find {}", err)
298    }
299
300    pub(crate) fn lookup_early_region(
301        &mut self,
302        span: Span,
303        region: &hax::EarlyParamRegion,
304    ) -> Result<RegionDbVar, Error> {
305        self.lookup_param(
306            span,
307            |bl| bl.early_region_vars.get(region).copied(),
308            || format!("the region variable {region:?}"),
309        )
310    }
311
312    pub(crate) fn lookup_late_param_region(
313        &mut self,
314        span: Span,
315        region: &hax::LateParamRegion,
316    ) -> Result<RegionDbVar, Error> {
317        let hax::LateParamRegionKind::Named(def_id, _) = &region.kind else {
318            raise_error!(self, span, "Unexpected late-bound region: {region:?}")
319        };
320        self.lookup_param(
321            span,
322            |bl| bl.region_vars_by_def_id.get(def_id).copied(),
323            || format!("the late-bound region variable {region:?}"),
324        )
325    }
326
327    pub(crate) fn lookup_type_var(
328        &mut self,
329        span: Span,
330        param: &hax::ParamTy,
331    ) -> Result<TypeDbVar, Error> {
332        self.lookup_param(
333            span,
334            |bl| bl.type_vars_map.get(&param.index).copied(),
335            || format!("the type variable {}", param.name),
336        )
337    }
338
339    pub(crate) fn lookup_const_generic_var(
340        &mut self,
341        span: Span,
342        param: &hax::ParamConst,
343    ) -> Result<ConstGenericDbVar, Error> {
344        self.lookup_param(
345            span,
346            |bl| bl.const_generic_vars_map.get(&param.index).copied(),
347            || format!("the const generic variable {}", param.name),
348        )
349    }
350
351    pub(crate) fn lookup_clause_var(
352        &mut self,
353        span: Span,
354        id: &hax::GenericPredicateId,
355    ) -> Result<ClauseDbVar, Error> {
356        self.lookup_param(
357            span,
358            |bl| bl.trait_preds.get(id).copied(),
359            || format!("the trait clause variable {id:?}"),
360        )
361    }
362
363    pub(crate) fn push_generic_params(&mut self, generics: &hax::TyGenerics) -> Result<(), Error> {
364        for param in &generics.params {
365            self.push_generic_param(param)?;
366        }
367        Ok(())
368    }
369
370    pub(crate) fn push_generic_param(&mut self, param: &hax::GenericParamDef) -> Result<(), Error> {
371        let variance = translate_variance(param.variance.as_ref());
372        match &param.kind {
373            hax::GenericParamDefKind::Lifetime => {
374                let region = hax::EarlyParamRegion {
375                    index: param.index,
376                    name: param.name,
377                };
378                let mutability = self
379                    .t_ctx
380                    .lt_mutability_computer
381                    .compute_lifetime_mutability(
382                        &self.hax_state,
383                        self.item_src.def_id(),
384                        param.index,
385                    );
386                let _ = self.innermost_binder_mut().push_early_region(
387                    region,
388                    param.def_id.clone(),
389                    variance,
390                    mutability,
391                );
392            }
393            hax::GenericParamDefKind::Type { .. } => {
394                let _ =
395                    self.innermost_binder_mut()
396                        .push_type_var(param.index, param.name, variance);
397            }
398            hax::GenericParamDefKind::Const { ty, .. } => {
399                let span = self.def_span(&param.def_id);
400                // The type should be primitive, meaning it shouldn't contain variables,
401                // non-primitive adts, etc. As a result, we can use an empty context.
402                let ty = self.translate_ty(span, ty)?;
403                self.innermost_binder_mut()
404                    .push_const_generic_var(param.index, ty, param.name);
405            }
406        }
407
408        Ok(())
409    }
410
411    // The parameters (and in particular the lifetimes) are split between
412    // early bound and late bound parameters. See those blog posts for explanations:
413    // https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/
414    // https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/
415    // Note that only lifetimes can be late bound at the moment.
416    //
417    // [TyCtxt.generics_of] gives us the early-bound parameters. We add the late-bound parameters
418    // here.
419    fn push_late_bound_generics_for_def(
420        &mut self,
421        _span: Span,
422        def: &hax::FullDef<'tcx>,
423    ) -> Result<(), Error> {
424        if let hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } = def.kind()
425        {
426            let innermost_binder = self.innermost_binder_mut();
427            assert!(innermost_binder.bound_region_vars.is_empty());
428            innermost_binder.push_params_from_binder(sig.rebind(()))?;
429        }
430        Ok(())
431    }
432
433    /// Add the generics and predicates of this item and its parents to the current context.
434    #[tracing::instrument(skip(self, span, def))]
435    fn push_generics_for_def(&mut self, span: Span, def: &hax::FullDef<'tcx>) -> Result<(), Error> {
436        trace!("{:?}", def.param_env());
437        // Add generics from the parent item, recursively (recursivity is important for closures,
438        // as they can be nested).
439        if let Some(parent_item) = def.typing_parent(self.hax_state()) {
440            let parent_def = self.hax_def(&parent_item)?;
441            self.push_generics_for_def(span, &parent_def)?;
442        }
443        self.push_generics_for_def_without_parents(span, def)?;
444        Ok(())
445    }
446
447    /// Add the generics and predicates of this item. This does not include the parent generics;
448    /// use `push_generics_for_def` to get the full list.
449    fn push_generics_for_def_without_parents(
450        &mut self,
451        _span: Span,
452        def: &hax::FullDef<'tcx>,
453    ) -> Result<(), Error> {
454        if let Some(param_env) = def.param_env() {
455            let origin = Self::predicate_origin_for_def(def);
456            self.push_param_env_without_parents(param_env, origin)?;
457        }
458
459        Ok(())
460    }
461
462    fn predicate_origin_for_def(def: &hax::FullDef<'tcx>) -> PredicateOrigin {
463        use crate::hax::FullDefKind;
464        match &def.kind {
465            FullDefKind::Adt { .. } | FullDefKind::TyAlias { .. } | FullDefKind::AssocTy { .. } => {
466                PredicateOrigin::WhereClauseOnType
467            }
468            FullDefKind::Fn { .. }
469            | FullDefKind::AssocFn { .. }
470            | FullDefKind::Closure { .. }
471            | FullDefKind::Const { .. }
472            | FullDefKind::AssocConst { .. }
473            | FullDefKind::Static { .. } => PredicateOrigin::WhereClauseOnFn,
474            FullDefKind::TraitImpl { .. } | FullDefKind::InherentImpl { .. } => {
475                PredicateOrigin::WhereClauseOnImpl
476            }
477            FullDefKind::Trait { .. } | FullDefKind::TraitAlias { .. } => {
478                PredicateOrigin::WhereClauseOnTrait
479            }
480            _ => panic!("Unexpected def: {:?}", def.def_id().kind),
481        }
482    }
483
484    fn push_param_env_without_parents(
485        &mut self,
486        param_env: &hax::ParamEnv,
487        origin: PredicateOrigin,
488    ) -> Result<(), Error> {
489        self.push_generic_params(&param_env.generics)?;
490        self.register_predicates(&param_env.predicates, origin)?;
491        Ok(())
492    }
493
494    /// Translate the generics and predicates of this item and its parents. This adds generic
495    /// parameters and predicates to the current environment (as a binder in
496    /// `self.binding_levels`). The constructed `GenericParams` can be recovered at the end using
497    /// `self.into_generics()` and stored in the translated item.
498    ///
499    /// On top of the generics introduced by `push_generics_for_def`, this adds extra parameters
500    /// required by the `TransItemSourceKind`.
501    pub fn translate_item_generics(
502        &mut self,
503        span: Span,
504        def: &hax::FullDef<'tcx>,
505        kind: &TransItemSourceKind,
506    ) -> Result<(), Error> {
507        assert!(self.binding_levels.is_empty());
508        self.binding_levels.push(BindingLevel::new());
509        self.push_generics_for_def(span, def)?;
510        self.push_late_bound_generics_for_def(span, def)?;
511
512        if let hax::FullDefKind::Closure { args, .. } = def.kind() {
513            // Add the lifetime generics coming from the upvars. We translate the upvar types early
514            // to know what lifetimes are needed.
515            let upvar_tys = self.translate_closure_upvar_tys(span, args)?;
516            // Add new lifetimes params to replace the erased ones.
517            let upvar_tys = upvar_tys.replace_erased_regions(|| {
518                let region_id = self.the_only_binder_mut().push_upvar_region();
519                Region::Var(DeBruijnVar::new_at_zero(region_id))
520            });
521            self.the_only_binder_mut().closure_upvar_tys = Some(upvar_tys);
522
523            // Add the lifetime generics coming from the higher-kindedness of the signature.
524            if let TransItemSourceKind::TraitImpl(TraitImplSource::Closure(..))
525            | TransItemSourceKind::ClosureMethod(..)
526            | TransItemSourceKind::ClosureAsFnCast = kind
527            {
528                self.the_only_binder_mut()
529                    .push_params_from_binder(args.fn_sig.rebind(()))?;
530            }
531            if let TransItemSourceKind::ClosureMethod(ClosureKind::Fn | ClosureKind::FnMut) = kind {
532                // Add the lifetime generics coming from the method itself.
533                let rid = self
534                    .the_only_binder_mut()
535                    .params
536                    .regions
537                    .push_with(|index| RegionParam::new(index, None, Variance::Covariant));
538                self.the_only_binder_mut().closure_call_method_region = Some(rid);
539            }
540        }
541
542        if matches!(
543            kind,
544            TransItemSourceKind::DropGlueMethod(..) | TransItemSourceKind::VTableDropShim
545        ) {
546            self.the_only_binder_mut().push_drop_glue_region();
547        }
548
549        self.innermost_binder_mut().params.check_consistency();
550        Ok(())
551    }
552
553    /// Push a new binding level, run the provided function inside it, then return the bound value.
554    pub(crate) fn inside_binder<F, U>(&mut self, kind: BinderKind, f: F) -> Result<Binder<U>, Error>
555    where
556        F: FnOnce(&mut Self) -> Result<U, Error>,
557    {
558        self.binding_levels.push(BindingLevel::new());
559
560        // Call the continuation. Important: do not short-circuit on error here.
561        let res = f(self);
562
563        // Reset
564        let params = self.binding_levels.pop().unwrap().params;
565
566        // Return
567        res.map(|skip_binder| Binder {
568            kind,
569            params,
570            skip_binder,
571        })
572    }
573
574    /// Push a new binding level corresponding to the provided `def` for the duration of the inner
575    /// function call.
576    pub(crate) fn translate_binder_for_def<F, U>(
577        &mut self,
578        span: Span,
579        kind: BinderKind,
580        def: &hax::FullDef<'tcx>,
581        f: F,
582    ) -> Result<Binder<U>, Error>
583    where
584        F: FnOnce(&mut Self) -> Result<U, Error>,
585    {
586        let inner_hax_state = self.t_ctx.hax_state.clone().with_hax_owner(def.def_id());
587        let outer_hax_state = mem::replace(&mut self.hax_state, inner_hax_state);
588        let ret = self.inside_binder(kind, |this| {
589            this.push_generics_for_def_without_parents(span, def)?;
590            this.push_late_bound_generics_for_def(span, def)?;
591            this.innermost_binder().params.check_consistency();
592            f(this)
593        });
594        self.hax_state = outer_hax_state;
595        ret
596    }
597
598    /// Push a new binding level corresponding to the provided item binder for the duration of the
599    /// inner function call.
600    pub(crate) fn translate_item_binder<F, T, U>(
601        &mut self,
602        _span: Span,
603        kind: BinderKind,
604        binder: &hax::TraitItemBinder<T>,
605        predicate_origin: PredicateOrigin,
606        f: F,
607    ) -> Result<Binder<U>, Error>
608    where
609        F: FnOnce(&mut Self, &T) -> Result<U, Error>,
610    {
611        let inner_hax_state = self.t_ctx.hax_state.clone().with_hax_owner(&binder.def_id);
612        let outer_hax_state = mem::replace(&mut self.hax_state, inner_hax_state);
613        let ret = self.inside_binder(kind, |this| {
614            this.push_param_env_without_parents(&binder.param_env, predicate_origin)?;
615            this.innermost_binder_mut()
616                .push_params_from_binder(binder.late_bound.clone())?;
617            this.innermost_binder().params.check_consistency();
618            f(this, &binder.skip_binder)
619        });
620        self.hax_state = outer_hax_state;
621        ret
622    }
623
624    /// Push a group of bound regions and call the continuation.
625    /// We use this when diving into a `for<'a>`, or inside an arrow type (because
626    /// it contains universally quantified regions).
627    pub(crate) fn translate_region_binder<F, T, U>(
628        &mut self,
629        _span: Span,
630        binder: &hax::Binder<T>,
631        f: F,
632    ) -> Result<RegionBinder<U>, Error>
633    where
634        F: FnOnce(&mut Self, &T) -> Result<U, Error>,
635    {
636        let binder = self.inside_binder(BinderKind::Other, |this| {
637            this.innermost_binder_mut()
638                .push_params_from_binder(binder.rebind(()))?;
639            f(this, binder.hax_skip_binder_ref())
640        })?;
641        // Convert to a region-only binder.
642        Ok(RegionBinder {
643            regions: binder.params.regions,
644            skip_binder: binder.skip_binder,
645        })
646    }
647
648    pub(crate) fn into_generics(mut self) -> GenericParams {
649        assert!(self.binding_levels.len() == 1);
650        self.binding_levels.pop().unwrap().params
651    }
652}
653
654/// Struct to compute the "mutability" of each lifetime.
655#[derive(Default)]
656pub struct LifetimeMutabilityComputer {
657    lt_mutability: HashMap<hax::DefId, CycleDetector<HashSet<u32>>>,
658}
659
660impl LifetimeMutabilityComputer {
661    /// Compute the mutability of one lifetime.
662    pub(crate) fn compute_lifetime_mutability<'tcx>(
663        &mut self,
664        s: &impl BaseState<'tcx>,
665        item: &hax::DefId,
666        index: u32,
667    ) -> LifetimeMutability {
668        match self.compute_lifetime_mutabilities(s, item) {
669            Some(set) => {
670                if set.contains(&index) {
671                    LifetimeMutability::Mutable
672                } else {
673                    LifetimeMutability::Shared
674                }
675            }
676            None => LifetimeMutability::Unknown,
677        }
678    }
679
680    /// Compute the "mutability" of each lifetime, i.e. whether this lifetime is used in a `&'a mut
681    /// T` type or not. Returns a set of the known-mutable lifetimes for this ADT.
682    fn compute_lifetime_mutabilities<'tcx>(
683        &mut self,
684        s: &impl BaseState<'tcx>,
685        item: &hax::DefId,
686    ) -> Option<&HashSet<u32>> {
687        if !matches!(
688            item.kind,
689            hax::DefKind::Struct | hax::DefKind::Enum | hax::DefKind::Union
690        ) {
691            return None;
692        }
693        if self
694            .lt_mutability
695            .entry(item.clone())
696            .or_default()
697            .start_processing()
698        {
699            use crate::hax::SInto;
700            use ty::{TypeSuperVisitable, TypeVisitable};
701
702            struct LtMutabilityVisitor<'a, S> {
703                s: &'a S,
704                computer: &'a mut LifetimeMutabilityComputer,
705                set: HashSet<u32>,
706            }
707            impl<'tcx, S: BaseState<'tcx>> ty::TypeVisitor<ty::TyCtxt<'tcx>> for LtMutabilityVisitor<'_, S> {
708                fn visit_ty(&mut self, ty: ty::Ty<'tcx>) {
709                    match ty.kind() {
710                        ty::Ref(r, _, ty::Mutability::Mut)
711                            if let ty::RegionKind::ReEarlyParam(r) = r.kind() =>
712                        {
713                            self.set.insert(r.index);
714                        }
715                        ty::Adt(adt, args) => {
716                            let item = adt.did().sinto(self.s);
717                            if let Some(mutabilities) =
718                                self.computer.compute_lifetime_mutabilities(self.s, &item)
719                            {
720                                for arg in args.iter() {
721                                    if let Some(r) = arg.as_region()
722                                        && let ty::RegionKind::ReEarlyParam(r) = r.kind()
723                                        && mutabilities.contains(&r.index)
724                                    {
725                                        self.set.insert(r.index);
726                                    }
727                                }
728                            }
729                        }
730                        _ => {}
731                    }
732                    ty.super_visit_with(self)
733                }
734            }
735            let mut visitor = LtMutabilityVisitor {
736                s,
737                computer: self,
738                set: HashSet::new(),
739            };
740
741            let tcx = s.base().tcx;
742            let def_id = item.real_rust_def_id();
743            let adt_def = tcx.adt_def(def_id);
744            let generics = item.identity_args(s);
745            for variant in adt_def.variants() {
746                for field in &variant.fields {
747                    field.ty(tcx, generics).visit_with(&mut visitor);
748                }
749            }
750            let set = visitor.set;
751
752            self.lt_mutability
753                .get_mut(item)
754                .unwrap()
755                .done_processing(set);
756        }
757        self.lt_mutability.get(item)?.as_processed()
758    }
759}
charon_driver/translate/translate_generics.rs

charon_driver/translate/
translate_generics.rs
