rapx/verify/
generic.rs

1//! Generic-parameter helpers for layout-sensitive verify checks.
2//!
3//! This is the verify-side version of the old Senryx generic helper.  It maps
4//! selected generic trait bounds to a finite set of representative concrete
5//! types, so SMT lowering can reason about layout requirements that mention
6//! generic parameters.
7
8use std::collections::{HashMap, HashSet};
9
10use if_chain::if_chain;
11use rustc_hir::{ImplPolarity, ItemId, ItemKind, hir_id::OwnerId};
12use rustc_middle::ty::{
13    ConstKind, FloatTy, GenericArgKind, IntTy, ParamEnv, Ty, TyCtxt, TyKind, UintTy,
14};
15
16/// Representative concrete types satisfying generic trait bounds.
17pub struct GenericTypeCandidates<'tcx> {
18    trait_map: HashMap<String, HashSet<Ty<'tcx>>>,
19}
20
21fn ty_has_param_const(ty: Ty<'_>) -> bool {
22    for arg in ty.walk() {
23        match arg.kind() {
24            GenericArgKind::Const(c) if matches!(c.kind(), ConstKind::Param(_)) => return true,
25            GenericArgKind::Type(inner_ty) if matches!(inner_ty.kind(), TyKind::Alias(..)) => {
26                return true;
27            }
28            _ => {}
29        }
30    }
31    false
32}
33
34impl<'tcx> GenericTypeCandidates<'tcx> {
35    /// Build generic type candidates from a function definition.
36    pub fn for_def(tcx: TyCtxt<'tcx>, def_id: rustc_hir::def_id::DefId) -> Self {
37        Self::new(tcx, tcx.param_env(def_id))
38    }
39
40    /// Build generic type candidates from a parameter environment.
41    pub fn new(tcx: TyCtxt<'tcx>, param_env: ParamEnv<'tcx>) -> Self {
42        let mut trait_bounds: HashMap<String, HashSet<String>> = HashMap::new();
43        let mut satisfied_types: HashMap<String, HashSet<Ty<'tcx>>> = HashMap::new();
44
45        for clause in param_env.caller_bounds() {
46            let Some(trait_clause) = clause.as_trait_clause() else {
47                continue;
48            };
49            let trait_def_id = trait_clause.def_id();
50            let generic_name = trait_clause.self_ty().skip_binder().to_string();
51            let trait_name = tcx.def_path_str(trait_def_id);
52            trait_bounds
53                .entry(generic_name.clone())
54                .or_default()
55                .insert(trait_name.clone());
56
57            let type_set = satisfied_types.entry(generic_name).or_default();
58            for impl_def_id in tcx.all_impls(trait_def_id) {
59                if !impl_def_id.is_local() {
60                    continue;
61                }
62                let impl_owner_id = tcx
63                    .hir_owner_node(OwnerId {
64                        def_id: impl_def_id.expect_local(),
65                    })
66                    .def_id();
67                let item = tcx.hir_item(ItemId {
68                    owner_id: impl_owner_id,
69                });
70                #[cfg(rapx_rustc_ge_193)]
71                let trait_ref_opt = tcx.impl_opt_trait_ref(impl_def_id);
72                #[cfg(not(rapx_rustc_ge_193))]
73                let trait_ref_opt = tcx.impl_trait_ref(impl_def_id);
74
75                if_chain! {
76                    if let ItemKind::Impl(impl_item) = item.kind;
77                    if let Some(trait_impl_header) = impl_item.of_trait;
78                    if trait_impl_header.polarity == ImplPolarity::Positive;
79                    if let Some(binder) = trait_ref_opt;
80                    then {
81                        let impl_ty = binder.skip_binder().self_ty();
82                        match impl_ty.kind() {
83                            TyKind::Adt(adt_def, _) => {
84                                let ty = tcx.type_of(adt_def.did()).skip_binder();
85                                if !ty_has_param_const(ty) {
86                                    type_set.insert(ty);
87                                }
88                            }
89                            TyKind::Param(_) => {}
90                            _ => {
91                                if !ty_has_param_const(impl_ty) {
92                                    type_set.insert(impl_ty);
93                                }
94                            }
95                        }
96                    }
97                }
98            }
99
100            if trait_name == "bytemuck::Pod" || trait_name == "plain::Plain" {
101                type_set.extend(Self::pod_types(tcx));
102            }
103        }
104
105        let std_marker_traits = HashSet::from([
106            String::from("std::marker::Copy"),
107            String::from("std::clone::Clone"),
108            String::from("std::marker::Sized"),
109        ]);
110        for (name, type_set) in &mut satisfied_types {
111            if trait_bounds
112                .get(name)
113                .map(|bounds| bounds.is_subset(&std_marker_traits))
114                .unwrap_or(false)
115            {
116                type_set.clear();
117            }
118        }
119
120        Self {
121            trait_map: satisfied_types,
122        }
123    }
124
125    /// Return the representative types for a generic parameter name.
126    pub fn candidates_for(&self, generic_name: &str) -> Option<&HashSet<Ty<'tcx>>> {
127        self.trait_map.get(generic_name)
128    }
129
130    /// Return representative types for a generic parameter type.
131    pub fn candidates_for_ty(&self, ty: Ty<'tcx>) -> Option<&HashSet<Ty<'tcx>>> {
132        let TyKind::Param(_) = ty.kind() else {
133            return None;
134        };
135        self.candidates_for(&ty.to_string())
136    }
137
138    fn pod_types(tcx: TyCtxt<'tcx>) -> HashSet<Ty<'tcx>> {
139        [
140            tcx.mk_ty_from_kind(TyKind::Int(IntTy::Isize)),
141            tcx.mk_ty_from_kind(TyKind::Int(IntTy::I8)),
142            tcx.mk_ty_from_kind(TyKind::Int(IntTy::I16)),
143            tcx.mk_ty_from_kind(TyKind::Int(IntTy::I32)),
144            tcx.mk_ty_from_kind(TyKind::Int(IntTy::I64)),
145            tcx.mk_ty_from_kind(TyKind::Int(IntTy::I128)),
146            tcx.mk_ty_from_kind(TyKind::Uint(UintTy::Usize)),
147            tcx.mk_ty_from_kind(TyKind::Uint(UintTy::U8)),
148            tcx.mk_ty_from_kind(TyKind::Uint(UintTy::U16)),
149            tcx.mk_ty_from_kind(TyKind::Uint(UintTy::U32)),
150            tcx.mk_ty_from_kind(TyKind::Uint(UintTy::U64)),
151            tcx.mk_ty_from_kind(TyKind::Uint(UintTy::U128)),
152            tcx.mk_ty_from_kind(TyKind::Float(FloatTy::F32)),
153            tcx.mk_ty_from_kind(TyKind::Float(FloatTy::F64)),
154        ]
155        .into_iter()
156        .collect()
157    }
158}
rapx/verify/generic.rs

rapx/verify/
generic.rs
