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::{ctx::TransformPass, TransformCtx};
8
9#[derive(Visitor)]
10struct RemoveMarkersVisitor {
11    exclude: HashSet<TraitDeclId>,
12}
13
14// Remove clauses and trait refs that mention the offending traits. This relies on the fact that
15// `Vector::remove` does not shift indices: it simply leaves an empty slot.
16// FIXME: this is a footgun, it caused at least https://github.com/AeneasVerif/charon/issues/561.
17impl VisitAstMut for RemoveMarkersVisitor {
18    fn enter_generic_params(&mut self, args: &mut GenericParams) {
19        let trait_clauses = &mut args.trait_clauses;
20        for i in trait_clauses.all_indices() {
21            let clause = &trait_clauses[i];
22            if self.exclude.contains(&clause.trait_.skip_binder.trait_id) {
23                trait_clauses.remove(i);
24            }
25        }
26    }
27    fn enter_generic_args(&mut self, args: &mut GenericArgs) {
28        let trait_refs = &mut args.trait_refs;
29        for i in trait_refs.all_indices() {
30            let tref = &trait_refs[i];
31            if self
32                .exclude
33                .contains(&tref.trait_decl_ref.skip_binder.trait_id)
34            {
35                trait_refs.remove(i);
36            }
37        }
38    }
39    fn enter_trait_decl(&mut self, tdecl: &mut TraitDecl) {
40        let trait_clauses = &mut tdecl.parent_clauses;
41        for i in trait_clauses.all_indices() {
42            let clause = &trait_clauses[i];
43            if self.exclude.contains(&clause.trait_.skip_binder.trait_id) {
44                trait_clauses.remove(i);
45            }
46        }
47    }
48    fn enter_trait_impl(&mut self, timpl: &mut TraitImpl) {
49        let trait_refs = &mut timpl.parent_trait_refs;
50        for i in trait_refs.all_indices() {
51            let tref = &trait_refs[i];
52            if self
53                .exclude
54                .contains(&tref.trait_decl_ref.skip_binder.trait_id)
55            {
56                trait_refs.remove(i);
57            }
58        }
59    }
60}
61
62pub struct Transform;
63impl TransformPass for Transform {
64    fn transform_ctx(&self, ctx: &mut TransformCtx) {
65        // Remove any mention of these traits in generic parameters and arguments.
66        // We always hide `Allocator` because in `Box` it refers to a type parameter that we always
67        // remove.
68        let exclude: &[_] = if ctx.options.hide_marker_traits {
69            &[
70                "core::marker::Sized",
71                "core::marker::Tuple",
72                "core::marker::Send",
73                "core::marker::Sync",
74                "core::marker::Unpin",
75                "core::alloc::Allocator",
76            ]
77        } else {
78            &["core::alloc::Allocator"]
79        };
80
81        let exclude: Vec<NamePattern> = exclude
82            .into_iter()
83            .map(|s| NamePattern::parse(s).unwrap())
84            .collect_vec();
85        let exclude: HashSet<TraitDeclId> = ctx
86            .translated
87            .item_names
88            .iter()
89            .filter(|(_, name)| exclude.iter().any(|p| p.matches(&ctx.translated, name)))
90            .filter_map(|(id, _)| id.as_trait_decl())
91            .copied()
92            .collect();
93
94        for &id in &exclude {
95            ctx.translated.trait_decls.remove(id);
96        }
97
98        let _ = ctx
99            .translated
100            .drive_mut(&mut RemoveMarkersVisitor { exclude });
101    }
102}
charon_lib/transform/hide_marker_traits.rs

charon_lib/transform/
hide_marker_traits.rs
