charon_lib/transform/simplify_output/
remove_adt_clauses.rs

1//! `--remove-adt-clauses` strips trait clauses from type declarations when it's possible to do so.
2//! Because it's not possible to recover associated type information when we remove clauses,
3//! we don't remove clauses if any of them have associated types. For that reason,
4//! this flag is best used with `--lift-associated-types`.
5//!
6//! Every reference to a clause removed in this way is replaced with a `TraitRefKind::BuiltinOrAuto
7//! { builtin_data: RemovedAdtClause, .. }`.
8
9use std::collections::HashSet;
10
11use crate::ast::*;
12use crate::ids::{IndexMap, IndexVec};
13use crate::transform::{TransformCtx, ctx::TransformPass};
14use crate::utils::CycleDetector;
15
16/// Compute whether a trait has associated types, even through supertraits.
17fn has_assoc_types(
18    translated: &TranslatedCrate,
19    cache: &mut IndexMap<TraitDeclId, CycleDetector<bool>>,
20    id: TraitDeclId,
21) -> bool {
22    if cache[id].start_processing() {
23        let result = match translated.trait_decls.get(id) {
24            Some(tdecl) => {
25                !tdecl.types.is_empty()
26                    || tdecl
27                        .implied_clauses
28                        .iter()
29                        .any(|p| has_assoc_types(translated, cache, p.trait_.skip_binder.id))
30            }
31            None => false,
32        };
33        cache[id].done_processing(result);
34    }
35    match &cache[id] {
36        CycleDetector::Processed(b) => *b,
37        CycleDetector::Cyclic | CycleDetector::Processing => false,
38        CycleDetector::Unprocessed => unreachable!(),
39    }
40}
41
42/// ADTs that have at least one trait clause pointing at a trait with associated types
43/// (transitively). We leave these ADTs entirely untouched.
44fn untouchable_adts(translated: &TranslatedCrate) -> HashSet<TypeDeclId> {
45    let mut cache: IndexMap<TraitDeclId, CycleDetector<bool>> = translated
46        .trait_decls
47        .map_ref_opt(|_| Some(CycleDetector::Unprocessed));
48    translated
49        .type_decls
50        .iter()
51        .filter(|d| {
52            d.generics
53                .trait_clauses
54                .iter()
55                .any(|c| has_assoc_types(translated, &mut cache, c.trait_.skip_binder.id))
56        })
57        .map(|d| d.def_id)
58        .collect()
59}
60
61#[derive(Visitor)]
62struct RemoveAdtClausesVisitor<'a> {
63    translated: &'a TranslatedCrate,
64    untouchable_adts: &'a HashSet<TypeDeclId>,
65    binder_stack: BindingStack<GenericParams>,
66}
67
68impl VisitorWithBinderStack for RemoveAdtClausesVisitor<'_> {
69    fn binder_stack_mut(&mut self) -> &mut BindingStack<GenericParams> {
70        &mut self.binder_stack
71    }
72}
73
74impl VisitAstMut for RemoveAdtClausesVisitor<'_> {
75    fn visit<T: AstVisitable>(&mut self, x: &mut T) -> ::std::ops::ControlFlow<Self::Break> {
76        VisitWithBinderStack::new(self).visit(x)?;
77        ::std::ops::ControlFlow::Continue(())
78    }
79
80    fn enter_type_decl(&mut self, decl: &mut TypeDecl) {
81        if self.untouchable_adts.contains(&decl.def_id) {
82            return;
83        }
84        decl.generics.trait_clauses.clear();
85        decl.generics.trait_type_constraints.clear();
86        // The wrapper has already pushed the (uncleared) generic params onto the binder stack.
87        // Replace the top with the cleared version so dangling-clause detection works as we
88        // descend into the body.
89        *self.binder_stack.innermost_mut() = decl.generics.clone();
90    }
91
92    fn enter_type_decl_ref(&mut self, tref: &mut TypeDeclRef) {
93        if !self.untouchable_adts.contains(&tref.id) {
94            tref.generics.trait_refs.clear();
95        }
96    }
97
98    fn enter_trait_ref(&mut self, tref: &mut TraitRef) {
99        let TraitRefKind::Clause(var) = &tref.kind else {
100            return;
101        };
102        if self
103            .binder_stack
104            .get_var::<_, GenericParams>(*var)
105            .is_some()
106        {
107            return;
108        }
109        let new_kind = build_removed_clause_placeholder(self.translated, &tref.trait_decl_ref);
110        tref.with_contents_mut(|contents| contents.kind = new_kind);
111    }
112}
113
114/// Build a `BuiltinOrAuto { builtin_data: RemovedAdtClause, .. }` kind whose `parent_trait_refs`
115/// recursively mirror the trait's implied clauses (each parent itself a `RemovedAdtClause`
116/// placeholder).
117///
118/// Substitution into the parents' `trait_decl_ref`s uses a stub placeholder kind for `Self`
119/// rather than the original (dangling) `Clause(var)`: otherwise we'd embed dangling clause refs
120/// inside the synthesized parents, and the visitor never re-enters them.
121fn build_removed_clause_placeholder(
122    translated: &TranslatedCrate,
123    trait_decl_ref: &PolyTraitDeclRef,
124) -> TraitRefKind {
125    let trait_id = trait_decl_ref.skip_binder.id;
126    let stub_tref = TraitRef::new(
127        TraitRefKind::BuiltinOrAuto {
128            builtin_data: BuiltinImplData::RemovedAdtClause,
129            vtable: None,
130            parent_trait_refs: Default::default(),
131            types: Default::default(),
132        },
133        trait_decl_ref.clone(),
134    );
135    let parent_trait_refs: IndexVec<TraitClauseId, TraitRef> = translated
136        .trait_decls
137        .get(trait_id)
138        .map(|tdecl| {
139            Substituted::new_for_trait_ref(&tdecl.implied_clauses, &stub_tref)
140                .iter()
141                .map(|s| {
142                    let parent: TraitParam = s.substitute();
143                    let kind = build_removed_clause_placeholder(translated, &parent.trait_);
144                    TraitRef::new(kind, parent.trait_)
145                })
146                .collect()
147        })
148        .unwrap_or_default();
149    TraitRefKind::BuiltinOrAuto {
150        builtin_data: BuiltinImplData::RemovedAdtClause,
151        vtable: None,
152        parent_trait_refs,
153        types: Default::default(),
154    }
155}
156
157pub struct Transform;
158impl TransformPass for Transform {
159    fn transform_ctx(&self, ctx: &mut TransformCtx) {
160        if !ctx.options.remove_adt_clauses {
161            return;
162        }
163        let untouchable = untouchable_adts(&ctx.translated);
164        ctx.for_each_item_mut(|ctx, mut item| {
165            let _ = item.drive_mut(&mut RemoveAdtClausesVisitor {
166                translated: &ctx.translated,
167                untouchable_adts: &untouchable,
168                binder_stack: BindingStack::empty(),
169            });
170        });
171    }
172}
charon_lib/transform/simplify_output/remove_adt_clauses.rs

charon_lib/transform/simplify_output/
remove_adt_clauses.rs
