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

charon_driver/translate/
translate_generics.rs
