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

charon_lib/transform/simplify_output/
remove_unused_clauses.rs
