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

charon_lib/transform/simplify_output/
remove_adt_clauses.rs
