charon_lib/transform/
hide_marker_traits.rs

1use derive_generic_visitor::*;
2use itertools::Itertools;
3use std::collections::HashSet;
4
5use crate::{ast::*, name_matcher::NamePattern};
6
7use super::{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, TraitClause>) {
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.parent_clauses);
46    }
47    fn enter_trait_impl(&mut self, timpl: &mut TraitImpl) {
48        self.filter_trait_refs(&mut timpl.parent_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 (_, _, trait_refs) in types {
59                self.filter_trait_refs(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            ]
80        } else {
81            vec![]
82        };
83        if ctx.options.hide_allocator {
84            exclude.push("core::alloc::Allocator");
85        }
86        if exclude.is_empty() {
87            return;
88        }
89
90        let exclude: Vec<NamePattern> = exclude
91            .into_iter()
92            .map(|s| NamePattern::parse(s).unwrap())
93            .collect_vec();
94        let exclude: HashSet<TraitDeclId> = ctx
95            .translated
96            .item_names
97            .iter()
98            .filter(|(_, name)| exclude.iter().any(|p| p.matches(&ctx.translated, name)))
99            .filter_map(|(id, _)| id.as_trait_decl())
100            .copied()
101            .collect();
102
103        for &id in &exclude {
104            ctx.translated.trait_decls.remove(id);
105        }
106
107        let _ = ctx
108            .translated
109            .drive_mut(&mut RemoveMarkersVisitor { exclude });
110    }
111}
charon_lib/transform/hide_marker_traits.rs

charon_lib/transform/
hide_marker_traits.rs
