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

charon_driver/translate/
translate_generics.rs
