charon_lib/transform/simplify_output/
hide_marker_traits.rs

1use derive_generic_visitor::*;
2use itertools::Itertools;
3use std::collections::HashSet;
4
5use crate::{ast::*, name_matcher::NamePattern};
6
7use crate::transform::{TransformCtx, ctx::TransformPass};
8
9#[derive(Visitor)]
10struct RemoveMarkersVisitor {
11    exclude: HashSet<TraitDeclId>,
12}
13
14impl RemoveMarkersVisitor {
15    fn filter_trait_refs(&mut self, trait_refs: &mut Vector<TraitClauseId, TraitRef>) {
16        for i in trait_refs.all_indices() {
17            let tref = &trait_refs[i];
18            if self.exclude.contains(&tref.trait_decl_ref.skip_binder.id) {
19                trait_refs.remove(i);
20            }
21        }
22    }
23
24    fn filter_trait_clauses(&mut self, trait_clauses: &mut Vector<TraitClauseId, TraitParam>) {
25        for i in trait_clauses.all_indices() {
26            let clause = &trait_clauses[i];
27            if self.exclude.contains(&clause.trait_.skip_binder.id) {
28                trait_clauses.remove(i);
29            }
30        }
31    }
32}
33
34// Remove clauses and trait refs that mention the offending traits. This relies on the fact that
35// `Vector::remove` does not shift indices: it simply leaves an empty slot.
36// FIXME: this is a footgun, it caused at least https://github.com/AeneasVerif/charon/issues/561.
37impl VisitAstMut for RemoveMarkersVisitor {
38    fn enter_generic_params(&mut self, args: &mut GenericParams) {
39        self.filter_trait_clauses(&mut args.trait_clauses);
40    }
41    fn enter_generic_args(&mut self, args: &mut GenericArgs) {
42        self.filter_trait_refs(&mut args.trait_refs);
43    }
44    fn enter_trait_decl(&mut self, tdecl: &mut TraitDecl) {
45        self.filter_trait_clauses(&mut tdecl.implied_clauses);
46    }
47    fn enter_trait_impl(&mut self, timpl: &mut TraitImpl) {
48        self.filter_trait_refs(&mut timpl.implied_trait_refs);
49    }
50    fn enter_trait_ref_kind(&mut self, x: &mut TraitRefKind) {
51        if let TraitRefKind::BuiltinOrAuto {
52            parent_trait_refs,
53            types,
54            ..
55        } = x
56        {
57            self.filter_trait_refs(parent_trait_refs);
58            for (_, assoc_ty) in types {
59                self.filter_trait_refs(&mut assoc_ty.implied_trait_refs);
60            }
61        }
62    }
63}
64
65pub struct Transform;
66impl TransformPass for Transform {
67    fn transform_ctx(&self, ctx: &mut TransformCtx) {
68        // We remove any mention of these traits in generic parameters and arguments.
69        let mut exclude = if ctx.options.hide_marker_traits {
70            vec![
71                "core::marker::Destruct",
72                "core::marker::PointeeSized",
73                "core::marker::MetaSized",
74                "core::marker::Sized",
75                "core::marker::Tuple",
76                "core::marker::Send",
77                "core::marker::Sync",
78                "core::marker::Unpin",
79                "core::clone::TrivialClone",
80            ]
81        } else {
82            vec![]
83        };
84        if ctx.options.hide_allocator {
85            exclude.push("core::alloc::Allocator");
86        }
87        if exclude.is_empty() {
88            return;
89        }
90
91        let exclude: Vec<NamePattern> = exclude
92            .into_iter()
93            .map(|s| NamePattern::parse(s).unwrap())
94            .collect_vec();
95        let exclude: HashSet<TraitDeclId> = ctx
96            .translated
97            .item_names
98            .iter()
99            .filter(|(_, name)| exclude.iter().any(|p| p.matches(&ctx.translated, name)))
100            .filter_map(|(id, _)| id.as_trait_decl())
101            .copied()
102            .collect();
103
104        // Remove the marker traits and their methods.
105        for &trait_id in &exclude {
106            if let Some(tdecl) = &ctx.translated.trait_decls.get(trait_id) {
107                for method in &tdecl.methods {
108                    ctx.translated.fun_decls.remove(method.skip_binder.item.id);
109                }
110            }
111            ctx.translated.trait_decls.remove(trait_id);
112        }
113        // Also remove any impls for these traits.
114        for impl_id in ctx.translated.trait_impls.all_indices() {
115            if let Some(timpl) = &ctx.translated.trait_impls.get(impl_id)
116                && exclude.contains(&timpl.impl_trait.id)
117            {
118                for (_, method) in &timpl.methods {
119                    ctx.translated.fun_decls.remove(method.skip_binder.id);
120                }
121                ctx.translated.trait_impls.remove(impl_id);
122            }
123        }
124
125        let _ = ctx
126            .translated
127            .drive_mut(&mut RemoveMarkersVisitor { exclude });
128    }
129}
charon_lib/transform/simplify_output/hide_marker_traits.rs

charon_lib/transform/simplify_output/
hide_marker_traits.rs
