charon_lib/transform/normalize/
normalize_trait_refs.rs

1use crate::{
2    ast::*,
3    ids::{IndexMap, IndexVec},
4    transform::{TransformCtx, ctx::TransformPass},
5};
6
7const MAX_NORMALIZATION_STEPS: usize = 100;
8
9#[derive(Visitor)]
10struct NormalizeTraitRefs<'a> {
11    impl_parent_refs: &'a IndexMap<TraitImplId, IndexVec<TraitClauseId, PolyTraitRef>>,
12    /// Charon can end up with self-referential clauses, see e.g.
13    /// `issue-1078-default-assoc-ty-self-ref-clause.rs`. Therefore we simply give up normalizing
14    /// after a number of steps.
15    steps: usize,
16}
17
18impl VisitAstMut for NormalizeTraitRefs<'_> {
19    fn visit_with_cached_type_info<T: AstVisitable>(
20        &mut self,
21        value: &mut WithCachedTypeInfo<T>,
22    ) -> ControlFlow<Self::Break> {
23        if value.type_info().is_normalized() {
24            ControlFlow::Continue(())
25        } else {
26            self.visit_inner(value)
27        }
28    }
29
30    fn exit_trait_ref(&mut self, tref: &mut TraitRef) {
31        if self.steps >= MAX_NORMALIZATION_STEPS {
32            return;
33        }
34        if let TraitRefKind::ParentClause(parent, clause_id, clause_args) = &tref.kind {
35            *tref = match &parent.kind {
36                TraitRefKind::TraitImpl(impl_ref) => {
37                    let Some(proof) = self.impl_parent_refs.get(impl_ref.id) else {
38                        return;
39                    };
40                    let mut proof = ItemBinder::new(impl_ref.id, proof[*clause_id].clone())
41                        .substitute(ItemBinder::new(CurrentItem, &impl_ref.generics))
42                        .under_current_binder()
43                        .apply(clause_args.clone());
44                    if *tref == proof {
45                        return;
46                    }
47                    // Recursively normalize.
48                    self.steps += 1;
49                    self.visit(&mut proof);
50                    proof
51                }
52                TraitRefKind::BuiltinOrAuto {
53                    parent_trait_refs, ..
54                } => {
55                    let Some(proof) = parent_trait_refs.get(*clause_id) else {
56                        return;
57                    };
58                    proof.clone().apply(clause_args.clone())
59                }
60                _ => return,
61            };
62        }
63    }
64}
65
66pub struct Transform;
67impl TransformPass for Transform {
68    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
69        !options.no_normalize
70    }
71
72    fn transform_ctx(&self, ctx: &mut TransformCtx) {
73        // Items are temporarily removed from the crate while we mutate them, so keep the original
74        // impl proofs separately.
75        let impl_parent_refs = ctx
76            .translated
77            .trait_impls
78            .map_ref(|timpl| timpl.implied_trait_refs.clone());
79        ctx.for_each_item_mut(|_, mut item| {
80            let _ = item.drive_mut(&mut NormalizeTraitRefs {
81                impl_parent_refs: &impl_parent_refs,
82                steps: 0,
83            });
84        });
85    }
86}
charon_lib/transform/normalize/normalize_trait_refs.rs

charon_lib/transform/normalize/
normalize_trait_refs.rs
