charon_driver/hax/types/
vars.rs

1use crate::hax::prelude::*;
2use crate::hax::sinto_as_usize;
3
4use enum_as_inner::EnumAsInner;
5use rustc_middle::ty;
6
7/// Reflects [`ty::ParamTy`]
8#[derive(Debug, Clone, PartialEq, Eq, Hash)]
9#[derive(AdtInto)]
10#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::ParamTy, state: S as gstate)]
11pub struct ParamTy {
12    pub index: u32,
13    pub name: Symbol,
14}
15
16/// Reflects [`ty::ParamConst`]
17#[derive(Debug, Clone, PartialEq, Eq, Hash)]
18#[derive(AdtInto)]
19#[args(<S>, from: ty::ParamConst, state: S as gstate)]
20pub struct ParamConst {
21    pub index: u32,
22    pub name: Symbol,
23}
24
25/// Reflects [`ty::BoundTyKind`]
26#[derive(Debug, Clone, PartialEq, Eq, Hash)]
27#[derive(AdtInto)]
28#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTyKind<'tcx>, state: S as s)]
29pub enum BoundTyKind {
30    Anon,
31    #[custom_arm(&FROM_TYPE::Param(def_id) => TO_TYPE::Param(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
32    Param(DefId, Symbol),
33}
34
35/// Reflects [`ty::BoundTy`]
36#[derive(Debug, Clone, PartialEq, Eq, Hash)]
37#[derive(AdtInto)]
38#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTy<'tcx>, state: S as s)]
39pub struct BoundTy {
40    pub var: BoundVar,
41    pub kind: BoundTyKind,
42}
43
44#[derive(Debug, Clone, PartialEq, Eq, Hash)]
45pub struct BoundTyRef {
46    pub index: BoundVarIndexKind,
47    pub ty: BoundTy,
48}
49
50sinto_as_usize!(rustc_middle::ty, BoundVar);
51
52/// Reflects [`ty::BoundRegionKind`]
53#[derive(Debug, Clone, PartialEq, Eq, Hash)]
54#[derive(AdtInto)]
55#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegionKind<'tcx>, state: S as s)]
56pub enum BoundRegionKind {
57    Anon,
58    NamedForPrinting(Symbol),
59    #[custom_arm(&FROM_TYPE::Named(def_id) => TO_TYPE::Named(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
60    Named(DefId, Symbol),
61    ClosureEnv,
62}
63
64/// Reflects [`ty::BoundRegion`]
65#[derive(Debug, Clone, PartialEq, Eq, Hash)]
66#[derive(AdtInto)]
67#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegion<'tcx>, state: S as s)]
68pub struct BoundRegion {
69    pub var: BoundVar,
70    pub kind: BoundRegionKind,
71}
72
73/// Reflects [`ty::PlaceholderRegion`]
74pub type PlaceholderRegion = Placeholder<BoundRegion>;
75/// Reflects [`ty::PlaceholderConst`]
76pub type PlaceholderConst = Placeholder<BoundVar>;
77/// Reflects [`ty::PlaceholderType`]
78pub type PlaceholderTy = Placeholder<BoundTy>;
79
80/// Reflects [`ty::Placeholder`]
81#[derive(Debug, Clone, PartialEq, Eq, Hash)]
82pub struct Placeholder<T> {
83    pub bound: T,
84}
85
86impl<'tcx, S: UnderOwnerState<'tcx>, T: SInto<S, U>, U> SInto<S, Placeholder<U>>
87    for ty::Placeholder<ty::TyCtxt<'tcx>, T>
88{
89    fn sinto(&self, s: &S) -> Placeholder<U> {
90        Placeholder {
91            bound: self.bound.sinto(s),
92        }
93    }
94}
95
96/// Reflects [`rustc_middle::infer::canonical::Canonical`]
97#[derive(Debug, Clone)]
98pub struct Canonical<T> {
99    pub value: T,
100}
101/// Reflects [`ty::CanonicalUserType`]
102pub type CanonicalUserType = Canonical<UserType>;
103
104impl<'tcx, S: UnderOwnerState<'tcx>, T: SInto<S, U>, U> SInto<S, Canonical<U>>
105    for rustc_middle::infer::canonical::Canonical<'tcx, T>
106{
107    fn sinto(&self, s: &S) -> Canonical<U> {
108        Canonical {
109            value: self.value.sinto(s),
110        }
111    }
112}
113
114/// Reflects [`ty::EarlyParamRegion`]
115#[derive(Debug, Clone, PartialEq, Eq, Hash)]
116#[derive(AdtInto)]
117#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::EarlyParamRegion, state: S as s)]
118pub struct EarlyParamRegion {
119    pub index: u32,
120    pub name: Symbol,
121}
122
123/// Reflects [`ty::LateParamRegion`]
124#[derive(Debug, Clone, PartialEq, Eq, Hash)]
125#[derive(AdtInto)]
126#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegion<'tcx>, state: S as s)]
127pub struct LateParamRegion {
128    pub scope: DefId,
129    pub kind: LateParamRegionKind,
130}
131
132/// Reflects [`ty::LateParamRegionKind`]
133#[derive(Debug, Clone, PartialEq, Eq, Hash)]
134#[derive(AdtInto)]
135#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegionKind, state: S as s)]
136pub enum LateParamRegionKind {
137    Anon(u32),
138    NamedAnon(u32, Symbol),
139    #[custom_arm(&FROM_TYPE::Named(def_id) => TO_TYPE::Named(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
140    Named(DefId, Symbol),
141    ClosureEnv,
142}
143
144/// Reflects [`ty::RegionKind`]
145#[derive(Debug, Clone, PartialEq, Eq, Hash)]
146#[derive(AdtInto)]
147#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::RegionKind<'tcx>, state: S as gstate)]
148pub enum RegionKind {
149    ReEarlyParam(EarlyParamRegion),
150    ReBound(BoundVarIndexKind, BoundRegion),
151    ReLateParam(LateParamRegion),
152    ReStatic,
153    ReVar(RegionVid),
154    RePlaceholder(PlaceholderRegion),
155    ReErased,
156    ReError(ErrorGuaranteed),
157}
158
159/// Reflects [`ty::BoundVarIndexKind`]
160#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
161#[derive(AdtInto)]
162#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundVarIndexKind, state: S as gstate)]
163pub enum BoundVarIndexKind {
164    Bound(DebruijnIndex),
165    Canonical,
166}
167
168sinto_as_usize!(rustc_middle::ty, DebruijnIndex);
169sinto_as_usize!(rustc_middle::ty, RegionVid);
170
171/// Reflects [`ty::Region`]
172#[derive(Debug, Clone, PartialEq, Eq, Hash)]
173#[derive(AdtInto)]
174#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::Region<'tcx>, state: S as s)]
175pub struct Region {
176    #[value(self.kind().sinto(s))]
177    pub kind: RegionKind,
178}
179
180/// Reflects both [`ty::GenericArg`] and [`ty::GenericArgKind`]
181#[derive(Debug, Clone, PartialEq, Eq, Hash)]
182#[derive(EnumAsInner)]
183#[derive(AdtInto)]
184#[args(< S: UnderOwnerState<'tcx>>, from: ty::GenericArgKind<'tcx>, state: S as s)]
185pub enum GenericArg<'tcx> {
186    Lifetime(Region),
187    Type(Ty<'tcx>),
188    Const(ConstantExpr<'tcx>),
189}
190
191impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, GenericArg<'tcx>> for ty::GenericArg<'tcx> {
192    fn sinto(&self, s: &S) -> GenericArg<'tcx> {
193        self.kind().sinto(s)
194    }
195}
196
197impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Vec<GenericArg<'tcx>>> for ty::GenericArgsRef<'tcx> {
198    fn sinto(&self, s: &S) -> Vec<GenericArg<'tcx>> {
199        self.iter().map(|v| v.kind().sinto(s)).collect()
200    }
201}
202
203/// Reflects partially [`ty::InferTy`]
204#[derive(Debug, Clone, PartialEq, Eq, Hash)]
205#[derive(AdtInto)]
206#[args(<'tcx, S>, from: ty::InferTy, state: S as gstate)]
207pub enum InferTy {
208    #[custom_arm(FROM_TYPE::TyVar(..) => TO_TYPE::TyVar,)]
209    TyVar, /*TODO?*/
210    #[custom_arm(FROM_TYPE::IntVar(..) => TO_TYPE::IntVar,)]
211    IntVar, /*TODO?*/
212    #[custom_arm(FROM_TYPE::FloatVar(..) => TO_TYPE::FloatVar,)]
213    FloatVar, /*TODO?*/
214    FreshTy(u32),
215    FreshIntTy(u32),
216    FreshFloatTy(u32),
217}
218
219/// Reflects [`ty::Variance`]
220#[derive(AdtInto)]
221#[args(<S>, from: ty::Variance, state: S as _s)]
222#[derive(Debug, Clone, PartialEq, Eq, Hash)]
223pub enum Variance {
224    Covariant,
225    Invariant,
226    Contravariant,
227    Bivariant,
228}
229
230/// Reflects [`ty::GenericParamDef`]
231#[derive(AdtInto)]
232#[args(< S: UnderOwnerState<'tcx>>, from: ty::GenericParamDef, state: S as s)]
233#[derive(Debug, Clone)]
234pub struct GenericParamDef<'tcx> {
235    pub name: Symbol,
236    pub def_id: DefId,
237    pub index: u32,
238    #[value(
239        match self.kind {
240            ty::GenericParamDefKind::Lifetime => GenericParamDefKind::Lifetime,
241            ty::GenericParamDefKind::Type { has_default, synthetic } => GenericParamDefKind::Type {
242                has_default,
243                synthetic,
244                inference_value: None,
245            },
246            ty::GenericParamDefKind::Const { has_default, .. } => {
247                let tcx = s.base().tcx;
248                let ty = if let Some(item) = s.owner().as_synthetic(s)
249                    && let Some(ty) = item.const_param_ty(s, self.index)
250                {
251                    // We use a dummy `DefId` for the generic params of synthetic items, so
252                    // `tcx.type_of` would be wrong.
253                    ty::Unnormalized::new(ty)
254                } else {
255                    tcx.type_of(self.def_id).instantiate_identity()
256                };
257                let ty = normalize(tcx, s.typing_env(), ty).sinto(s);
258                GenericParamDefKind::Const { has_default, ty }
259            },
260        }
261    )]
262    pub kind: GenericParamDefKind<'tcx>,
263    /// Variance of this type parameter, if sensible.
264    #[value({
265        use SyntheticItem::*;
266        use rustc_hir::def::DefKind::*;
267        let tcx = s.base().tcx;
268        match s.owner().as_synthetic(s) {
269            Some(Array | Slice | Tuple(_) | Str) => Some(Variance::Covariant),
270            // We could compute it but we won't need it since this item is only used in impls.
271            Some(FnPtr(_)) => None,
272            None => {
273                let parent = tcx.parent(self.def_id);
274                match tcx.def_kind(parent) {
275                    Fn | AssocFn | Enum | Struct | Union | Ctor(..) | OpaqueTy => {
276                        tcx.variances_of(parent).get(self.index as usize).sinto(s)
277                    }
278                    _ => None,
279                }
280            }
281        }
282    })]
283    pub variance: Option<Variance>,
284}
285
286/// Reflects [`ty::GenericParamDefKind`]
287#[derive(Debug, Clone)]
288pub enum GenericParamDefKind<'tcx> {
289    Lifetime,
290    Type {
291        has_default: bool,
292        synthetic: bool,
293        /// Closures and inline consts use special type parameters for inference purposes. Their
294        /// value is known after analysis, which we store here.
295        inference_value: Option<Ty<'tcx>>,
296    },
297    Const {
298        has_default: bool,
299        ty: Ty<'tcx>,
300    },
301}
302
303/// Reflects [`ty::Generics`]
304#[derive(AdtInto)]
305#[args(< S: UnderOwnerState<'tcx>>, from: ty::Generics, state: S as state)]
306#[derive(Debug, Clone)]
307pub struct TyGenerics<'tcx> {
308    pub parent: Option<DefId>,
309    pub parent_count: usize,
310    #[from(own_params)]
311    pub params: Vec<GenericParamDef<'tcx>>,
312}
313
314pub type UnitBinder<'tcx> = ty::Binder<'tcx, ()>;
315
316/// Reflects [`ty::BoundVariableKind`]
317#[derive(AdtInto)]
318#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundVariableKind<'tcx>, state: S as tcx)]
319#[derive(Debug, Clone, PartialEq, Eq, Hash)]
320pub enum BoundVariableKind {
321    Ty(BoundTyKind),
322    #[custom_arm(
323        &FROM_TYPE::Region(region) => TO_TYPE::Region(region.sinto(tcx), None),
324    )]
325    Region(BoundRegionKind, Option<Variance>),
326    Const,
327}
328
329/// Reflects [`ty::Binder`]
330#[derive(Debug, Clone, PartialEq, Eq, Hash)]
331pub struct Binder<T> {
332    pub value: T,
333    pub bound_vars: Vec<BoundVariableKind>,
334}
335
336impl Binder<()> {
337    pub fn empty() -> Self {
338        Binder {
339            value: (),
340            bound_vars: vec![],
341        }
342    }
343}
344
345impl<T> Binder<T> {
346    pub fn as_ref(&self) -> Binder<&T> {
347        Binder {
348            value: &self.value,
349            bound_vars: self.bound_vars.clone(),
350        }
351    }
352
353    pub fn hax_skip_binder(self) -> T {
354        self.value
355    }
356
357    pub fn hax_skip_binder_ref(&self) -> &T {
358        &self.value
359    }
360
361    pub fn map<U>(self, f: impl FnOnce(T) -> U) -> Binder<U> {
362        Binder {
363            value: f(self.value),
364            bound_vars: self.bound_vars,
365        }
366    }
367
368    pub fn inner_mut(&mut self) -> &mut T {
369        &mut self.value
370    }
371
372    pub fn rebind<U>(&self, value: U) -> Binder<U> {
373        self.as_ref().map(|_| value)
374    }
375}
376
377/// A representation of `exists<T: Trait1 + Trait2>(value)`: we create a fresh type id and the
378/// appropriate trait clauses. The contained value may refer to the fresh ty and the in-scope trait
379/// clauses. This is used to represent types related to `dyn Trait`.
380#[derive(Debug, Clone, PartialEq, Eq, Hash)]
381pub struct DynBinder<'tcx, T> {
382    /// Fresh type parameter that we use as the `Self` type in the predicates below.
383    pub existential_ty: ParamTy,
384    /// Clauses that define the trait object. These clauses use the fresh type parameter above
385    /// as `Self` type.
386    pub predicates: GenericPredicates<'tcx>,
387    /// The value inside the binder.
388    pub val: T,
389}
390
391impl<'tcx, S, T, U> SInto<S, DynBinder<'tcx, U>>
392    for rustc_trait_elaboration::DynBinder<'tcx, T, DefId>
393where
394    S: UnderOwnerState<'tcx>,
395    T: SInto<S, U>,
396{
397    fn sinto(&self, s: &S) -> DynBinder<'tcx, U> {
398        DynBinder {
399            existential_ty: self.existential_ty.sinto(s),
400            predicates: GenericPredicates {
401                predicates: self.predicates.sinto(s),
402            },
403            val: self.val.sinto(s),
404        }
405    }
406}
407
408/// Lets types declare how to compute the variance of bound parameters.
409trait BinderVariances<'tcx>: Sized {
410    fn variances(
411        _tcx: ty::TyCtxt<'tcx>,
412        _binder: &ty::Binder<'tcx, Self>,
413    ) -> HashMap<ty::BoundVar, ty::Variance> {
414        HashMap::default()
415    }
416}
417
418impl<'tcx> BinderVariances<'tcx> for ty::FnSig<'tcx> {
419    fn variances(
420        tcx: ty::TyCtxt<'tcx>,
421        binder: &ty::Binder<'tcx, Self>,
422    ) -> HashMap<ty::BoundVar, ty::Variance> {
423        fn_sig_bound_region_variances(tcx, *binder)
424    }
425}
426
427impl<'tcx> BinderVariances<'tcx> for ty::Ty<'tcx> {}
428impl<'tcx> BinderVariances<'tcx> for ty::ClauseKind<'tcx> {}
429impl<'tcx> BinderVariances<'tcx> for ty::PredicateKind<'tcx> {}
430impl<'tcx> BinderVariances<'tcx> for ty::TraitRef<'tcx> {}
431impl<'tcx> BinderVariances<'tcx> for ty::TraitClause<'tcx> {}
432impl<'tcx> BinderVariances<'tcx> for UserAnnotationData<'tcx> {}
433
434impl<'tcx, S: UnderOwnerState<'tcx>, T1, T2> SInto<S, Binder<T2>> for ty::Binder<'tcx, T1>
435where
436    T1: SInto<(StateWithOwner<'tcx>, UnitBinder<'tcx>), T2> + BinderVariances<'tcx>,
437{
438    fn sinto(&self, s: &S) -> Binder<T2> {
439        let variances = T1::variances(s.base().tcx, self);
440        let mut bound_vars = self.bound_vars().sinto(s);
441        for (index, var) in bound_vars.iter_mut().enumerate() {
442            if let BoundVariableKind::Region(_, variance) = var {
443                *variance = variances
444                    .get(&ty::BoundVar::from_usize(index))
445                    .copied()
446                    .sinto(s);
447            }
448        }
449        let value = {
450            // Keep the binder in the context, for when we translate predicates and such. This
451            // erases a preexisting binder in context, which is fine because we only need it
452            // immediately.
453            let under_binder_s = (s.as_state_with_owner(), self.as_ref().map_bound(|_| ()));
454            self.as_ref().skip_binder().sinto(&under_binder_s)
455        };
456        Binder { value, bound_vars }
457    }
458}
charon_driver/hax/types/vars.rs

charon_driver/hax/types/
vars.rs
