charon_driver/translate/
translate_generics.rs

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

charon_driver/translate/
translate_generics.rs
