charon_lib/transform/simplify_output/
remove_unused_clauses.rs

1//! Remove unused trait clauses from items. A clause is unused if it is only used to build proofs
2//! for other unused clauses.
3use derive_generic_visitor::*;
4use petgraph::visit::Walker;
5use petgraph::{graphmap::DiGraphMap, visit::Dfs};
6use std::collections::{HashMap, HashSet};
7
8use crate::ast::*;
9use crate::ids::IndexVec;
10
11use crate::transform::{TransformCtx, ctx::TransformPass};
12
13#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
14enum ClauseNode {
15    /// A special node to indicate clauses that we consider unconditionally used. Unused clauses
16    /// will in the end be the ones unreachable from the root.
17    Root,
18    /// The nth clause parameter of that item.
19    Clause(ItemId, TraitClauseId),
20}
21
22#[derive(Visitor)]
23struct BuildGraphVisitor<'a> {
24    graph: &'a mut DiGraphMap<ClauseNode, ()>,
25    /// The item we're visiting.
26    current_item: ItemId,
27    /// The node currently using the part of the AST we're visiting.
28    current_context: ClauseNode,
29    binder_depth: DeBruijnId,
30}
31
32impl VisitorWithBinderDepth for BuildGraphVisitor<'_> {
33    fn binder_depth_mut(&mut self) -> &mut DeBruijnId {
34        &mut self.binder_depth
35    }
36}
37
38impl VisitorWithItemRef for BuildGraphVisitor<'_> {
39    fn visit_item_ref(
40        &mut self,
41        item_id: ItemId,
42        args: &GenericArgs,
43    ) -> ControlFlow<<Self as Visitor>::Break> {
44        let GenericArgs {
45            regions,
46            types,
47            const_generics,
48            trait_refs,
49        } = args;
50        self.visit(regions)?;
51        self.visit(types)?;
52        self.visit(const_generics)?;
53        let old_context = self.current_context;
54        for (clause_id, trait_ref) in trait_refs.iter_enumerated() {
55            self.current_context = ClauseNode::Clause(item_id, clause_id);
56            self.visit(trait_ref)?;
57        }
58        self.current_context = old_context;
59        Continue(())
60    }
61}
62
63impl VisitAst for BuildGraphVisitor<'_> {
64    fn visit<T: AstVisitable>(&mut self, x: &T) -> ControlFlow<Self::Break> {
65        VisitWithBinderDepth::new(VisitWithItemRef::new(self)).visit(x)
66    }
67
68    fn visit_trait_param(&mut self, x: &TraitParam) -> ControlFlow<Self::Break> {
69        // Check if this is a clause definition at the level of the item. If so, we want to track
70        // inter-clause dependencies such as `TraitClause1: (TraitClause0::Item: Copy)`.
71        if self.binder_depth == DeBruijnId::ZERO && x.origin != PredicateOrigin::WhereClauseOnTrait
72        {
73            let old_context = self.current_context;
74            self.current_context = ClauseNode::Clause(self.current_item, x.clause_id);
75            self.visit(&x.trait_)?;
76            self.current_context = old_context;
77            Continue(())
78        } else {
79            self.visit_inner(x)
80        }
81    }
82
83    fn enter_trait_ref_kind(&mut self, x: &TraitRefKind) {
84        if let TraitRefKind::Clause(var) = x
85            && let Some(clause_id) = var.bound_at_depth(self.binder_depth)
86        {
87            self.graph.add_edge(
88                self.current_context,
89                ClauseNode::Clause(self.current_item, clause_id),
90                (),
91            );
92        }
93    }
94}
95
96#[derive(Visitor)]
97struct RemoveClausesVisitor<'a> {
98    /// For each item, a map from old clause ids to new ones. The new ones are in the same order,
99    /// just skipping some removed old ones.
100    remaps: &'a HashMap<ItemId, IndexVec<TraitClauseId, Option<TraitClauseId>>>,
101    current_item: ItemId,
102    binder_depth: DeBruijnId,
103}
104
105impl VisitorWithBinderDepth for RemoveClausesVisitor<'_> {
106    fn binder_depth_mut(&mut self) -> &mut DeBruijnId {
107        &mut self.binder_depth
108    }
109}
110
111impl VisitorWithItemRefMut for RemoveClausesVisitor<'_> {
112    fn enter_item_ref(&mut self, item_id: ItemId, args: &mut GenericArgs) {
113        if let Some(remap) = self.remaps.get(&item_id) {
114            for (old_id, trait_ref) in std::mem::take(&mut args.trait_refs).into_iter_enumerated() {
115                if remap[old_id].is_some() {
116                    args.trait_refs.push(trait_ref);
117                }
118            }
119        }
120    }
121}
122
123impl VisitAstMut for RemoveClausesVisitor<'_> {
124    fn visit<T: AstVisitable>(&mut self, x: &mut T) -> ControlFlow<Self::Break> {
125        VisitWithBinderDepth::new(VisitWithItemRef::new(self)).visit(x)
126    }
127
128    fn visit_trait_ref_kind(&mut self, x: &mut TraitRefKind) -> ControlFlow<Self::Break> {
129        if let TraitRefKind::Clause(var) = x
130            && let Some(clause_id) = var.bound_at_depth_mut(self.binder_depth)
131            && let Some(remap) = self.remaps.get(&self.current_item)
132        {
133            *clause_id = remap[*clause_id].expect("mismatch while trying to remove unused clauses");
134        }
135        self.visit_inner(x)
136    }
137}
138
139pub struct Transform;
140impl TransformPass for Transform {
141    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
142        options.remove_unused_clauses || options.remove_unused_self_clauses
143    }
144
145    fn transform_ctx(&self, ctx: &mut TransformCtx) {
146        // Build a dependency graph between all item clauses of the crate.
147        let graph: DiGraphMap<ClauseNode, ()> = {
148            let mut graph = DiGraphMap::new();
149            for item in ctx.translated.all_items() {
150                let item_id = item.id();
151                let is_opaque_fn = item.as_fun().is_some_and(|decl| !decl.body.has_contents());
152
153                for clause in &item.generic_params().trait_clauses {
154                    // For opaque bodies, we must assume they may be using any clause in scope.
155                    let may_remove_clause = !is_opaque_fn
156                        && (ctx.options.remove_unused_clauses
157                            || (ctx.options.remove_unused_self_clauses
158                                && clause.origin == PredicateOrigin::TraitSelf));
159                    if !may_remove_clause {
160                        let clause_id = clause.clause_id;
161                        graph.add_edge(
162                            ClauseNode::Root,
163                            ClauseNode::Clause(item_id, clause_id),
164                            (),
165                        );
166                    }
167                }
168
169                let mut visitor = BuildGraphVisitor {
170                    graph: &mut graph,
171                    current_item: item_id,
172                    binder_depth: DeBruijnId::ZERO,
173                    current_context: ClauseNode::Root,
174                };
175                item.drive(&mut visitor);
176            }
177            graph
178        };
179
180        // Remove the unused clauses and collect a global remapping of clause ids.
181        let remaps: HashMap<ItemId, IndexVec<TraitClauseId, Option<TraitClauseId>>> = {
182            let reachable: HashSet<ClauseNode> =
183                Dfs::new(&graph, ClauseNode::Root).iter(&graph).collect();
184            ctx.translated
185                .all_items_mut()
186                .filter_map(|mut item| {
187                    let item_id = item.as_ref().id();
188                    let item_clauses = &mut item.generic_params().trait_clauses;
189                    let clauses_to_remove: HashSet<TraitClauseId> = item_clauses
190                        .indices()
191                        .filter(|clause_id| {
192                            !reachable.contains(&ClauseNode::Clause(item_id, *clause_id))
193                        })
194                        .collect();
195                    if clauses_to_remove.is_empty() {
196                        return None;
197                    }
198                    let remap: IndexVec<TraitClauseId, Option<TraitClauseId>> =
199                        std::mem::take(item_clauses).map_indexed(|old_id, mut clause| {
200                            if clauses_to_remove.contains(&old_id) {
201                                None
202                            } else {
203                                let new_id = item_clauses.push_with(|new_id| {
204                                    clause.clause_id = new_id;
205                                    clause
206                                });
207                                Some(new_id)
208                            }
209                        });
210                    Some((item_id, remap))
211                })
212                .collect()
213        };
214
215        // Adjust references to clauses.
216        for mut item in ctx.translated.all_items_mut() {
217            let item_id = item.as_ref().id();
218            item.drive_mut(&mut RemoveClausesVisitor {
219                remaps: &remaps,
220                current_item: item_id,
221                binder_depth: DeBruijnId::ZERO,
222            });
223        }
224    }
225}
charon_lib/transform/simplify_output/remove_unused_clauses.rs

charon_lib/transform/simplify_output/
remove_unused_clauses.rs
