charon_lib/transform/add_missing_info/
add_missing_alias_clauses.rs

1//! Rust doesn't require bounds on type aliases to be well-formed. When a type alias mentions
2//! `<T as Trait>::Assoc` without a corresponding `T: Trait` clause, translation leaves an unknown
3//! trait ref. This pass tries to add these missing clauses.
4
5use crate::ast::*;
6use crate::transform::{TransformCtx, ctx::TransformPass};
7
8#[derive(Visitor)]
9struct ClauseExtractor<'a> {
10    params: &'a mut GenericParams,
11    span: Span,
12    binder_stack: BindingStack<GenericParams>,
13}
14
15impl<'a> ClauseExtractor<'a> {
16    fn new(params: &'a mut GenericParams, span: Span) -> Self {
17        Self {
18            binder_stack: BindingStack::new(params.clone()),
19            params,
20            span,
21        }
22    }
23
24    /// Move a trait ref out of the binders to make it a trait clause. Collects all the region
25    /// binders on the way to here into a single binder to make a HRTB.
26    fn extract_trait_clause(&self, mut trait_: PolyTraitDeclRef) -> Option<PolyTraitDeclRef> {
27        // Iterate over the binders on the way to this trait ref, skipping the first binder (the
28        // item binder).
29        let mut scope_regions = Vec::new();
30        for (dbid, params) in self.binder_stack.iter_enumerated().rev().skip(1) {
31            for (old_id, region) in params.regions.iter_enumerated() {
32                let new_id = trait_.regions.push_with(|index| {
33                    let mut region = region.clone();
34                    region.index = index;
35                    region
36                });
37                scope_regions.push((dbid, old_id, new_id));
38            }
39        }
40
41        if !scope_regions.is_empty() {
42            // Make all the region variables point at the outer binder.
43            #[derive(Visitor)]
44            struct MoveRegionsToHrtb {
45                binder_depth: DeBruijnId,
46                scope_regions: Vec<(DeBruijnId, RegionId, RegionId)>,
47            }
48
49            impl VisitorWithBinderDepth for MoveRegionsToHrtb {
50                fn binder_depth_mut(&mut self) -> &mut DeBruijnId {
51                    &mut self.binder_depth
52                }
53            }
54
55            impl VisitAstMut for MoveRegionsToHrtb {
56                fn visit<T: AstVisitable>(&mut self, x: &mut T) -> ControlFlow<Self::Break> {
57                    VisitWithBinderDepth::new(self).visit(x)
58                }
59
60                fn enter_region(&mut self, region: &mut Region) {
61                    let Region::Var(var) = region else {
62                        return;
63                    };
64                    let DeBruijnVar::Bound(dbid, old_id) = *var else {
65                        return;
66                    };
67                    let Some(outer_depth) = dbid.sub(self.binder_depth.incr()) else {
68                        return;
69                    };
70                    let Some((_, _, new_id)) = self
71                        .scope_regions
72                        .iter()
73                        .find(|(dbid, id, _)| *dbid == outer_depth && *id == old_id)
74                    else {
75                        return;
76                    };
77                    *var = DeBruijnVar::bound(self.binder_depth, *new_id);
78                }
79            }
80
81            MoveRegionsToHrtb {
82                binder_depth: DeBruijnId::zero(),
83                scope_regions,
84            }
85            .visit(&mut trait_.skip_binder);
86        }
87
88        trait_.move_from_under_binders(self.binder_stack.depth())
89    }
90}
91
92impl VisitorWithBinderStack for ClauseExtractor<'_> {
93    fn binder_stack_mut(&mut self) -> &mut BindingStack<GenericParams> {
94        &mut self.binder_stack
95    }
96}
97
98impl VisitAstMut for ClauseExtractor<'_> {
99    fn visit<T: AstVisitable>(&mut self, x: &mut T) -> ControlFlow<Self::Break> {
100        VisitWithBinderStack::new(self).visit(x)
101    }
102
103    fn exit_trait_ref_contents(&mut self, tref: &mut TraitRefContents) {
104        if matches!(tref.kind, TraitRefKind::Unknown(_))
105            && let Some(trait_) = self.extract_trait_clause(tref.trait_decl_ref.clone())
106        {
107            let clause_id = self.params.trait_clauses.push_with(|clause_id| TraitParam {
108                clause_id,
109                span: Some(self.span),
110                origin: PredicateOrigin::WhereClauseOnType,
111                trait_,
112            });
113            tref.kind =
114                TraitRefKind::Clause(DeBruijnVar::bound(self.binder_stack.depth(), clause_id));
115        }
116    }
117}
118
119pub struct Transform;
120impl TransformPass for Transform {
121    fn transform_ctx(&self, ctx: &mut TransformCtx) {
122        for tdecl in &mut ctx.translated.type_decls {
123            if let TypeDeclKind::Alias(ty) = &mut tdecl.kind {
124                ClauseExtractor::new(&mut tdecl.generics, tdecl.item_meta.span).visit(ty);
125            }
126        }
127    }
128}
charon_lib/transform/add_missing_info/add_missing_alias_clauses.rs

charon_lib/transform/add_missing_info/
add_missing_alias_clauses.rs
