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 let Some(id) = tref.as_adt()
94            && !self.untouchable_adts.contains(&id)
95        {
96            tref.generics.trait_refs.clear();
97        }
98    }
99
100    fn enter_trait_ref(&mut self, tref: &mut TraitRef) {
101        let TraitRefKind::Clause(var) = &tref.kind else {
102            return;
103        };
104        if self
105            .binder_stack
106            .get_var::<_, GenericParams>(*var)
107            .is_some()
108        {
109            return;
110        }
111        let new_kind = build_removed_clause_placeholder(self.translated, &tref.trait_decl_ref);
112        tref.with_contents_mut(|contents| contents.kind = new_kind);
113    }
114}
115
116/// Build a `BuiltinOrAuto { builtin_data: RemovedAdtClause, .. }` kind whose `parent_trait_refs`
117/// recursively mirror the trait's implied clauses (each parent itself a `RemovedAdtClause`
118/// placeholder).
119///
120/// Substitution into the parents' `trait_decl_ref`s uses a stub placeholder kind for `Self`
121/// rather than the original (dangling) `Clause(var)`: otherwise we'd embed dangling clause refs
122/// inside the synthesized parents, and the visitor never re-enters them.
123fn build_removed_clause_placeholder(
124    translated: &TranslatedCrate,
125    trait_decl_ref: &PolyTraitDeclRef,
126) -> TraitRefKind {
127    let trait_id = trait_decl_ref.skip_binder.id;
128    let stub_tref = TraitRef::new(
129        TraitRefKind::BuiltinOrAuto {
130            builtin_data: BuiltinImplData::RemovedAdtClause,
131            parent_trait_refs: Default::default(),
132            types: Default::default(),
133        },
134        trait_decl_ref.clone(),
135    );
136    let parent_trait_refs: IndexVec<TraitClauseId, TraitRef> = translated
137        .trait_decls
138        .get(trait_id)
139        .map(|tdecl| {
140            Substituted::new_for_trait_ref(&tdecl.implied_clauses, &stub_tref)
141                .iter()
142                .map(|s| {
143                    let parent: TraitParam = s.substitute();
144                    let kind = build_removed_clause_placeholder(translated, &parent.trait_);
145                    TraitRef::new(kind, parent.trait_)
146                })
147                .collect()
148        })
149        .unwrap_or_default();
150    TraitRefKind::BuiltinOrAuto {
151        builtin_data: BuiltinImplData::RemovedAdtClause,
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
