hax_frontend_exporter/
state.rs

1use crate::prelude::*;
2use paste::paste;
3
4macro_rules! mk_aux {
5    ($state:ident {$($lts:lifetime)*} $field:ident {$($field_type:tt)+} {$($gen:tt)*} {$($gen_full:tt)*} {$($params:tt)*} {$($fields:tt)*}) => {
6        paste ! {
7            pub trait [<Has $field:camel>]<$($lts,)*> {
8                fn $field(self: &Self) -> $($field_type)+<$($lts)*>;
9            }
10            impl<$($lts,)*$($gen)*> [<Has $field:camel>]<$($lts,)*> for $state<$($params)*> {
11                fn $field(self: &Self) -> $($field_type)+<$($lts)*> {
12                    self.$field.clone()
13                }
14            }
15            pub trait [<Has $field:camel Setter>]<$($lts)*> {
16                type Out;
17                // fn [<with_ $field>]<$($lts,)*$($gen)*>(self: Self, $field: $($field_type)+<$($lts)*>) -> $state<$($params)*>;
18                fn [<with_ $field>](self: Self, $field: $($field_type)+<$($lts)*>) -> Self::Out;
19            }
20            // const _: &str = stringify!(
21            #[allow(unused)]
22            impl<$($lts,)*$($gen_full)*> [<Has $field:camel Setter>]<$($lts,)*> for $state<$($gen_full)*> {
23                type Out = $state<$($params)*>;
24                fn [<with_ $field>](self: Self, $field: $($field_type)+<$($lts)*>) -> Self::Out {
25                    let __this_field = $field;
26                    let $state { $($fields,)* } = self;
27                    let $field = __this_field;
28                    $state { $($fields,)* }
29                }
30            }
31            // );
32            // pub trait [<Has $field:camel Setter>]<$($lts,)*$($gen_full)*> {
33            //     fn [<with_ $field>](self: Self, $field: $($field_type)+<$($lts)*>) -> $state<$($params)*>;
34            // }
35            // impl<$($lts,)*$($gen_full)*> [<Has $field:camel Setter>]<$($lts,)*$($gen_full)*> for $state<$($gen_full)*> {
36            //     fn [<with_ $field>](self: Self, $field: $($field_type)+<$($lts)*>) -> $state<$($params)*> {
37            //         let __this_field = $field;
38            //         let $state { $($fields,)* } = self;
39            //         let $field = __this_field;
40            //         $state { $($fields,)* }
41            //     }
42            // }
43        }
44    };
45}
46macro_rules! mk_is_state_trait {
47    ($lts:tt {$($finished:tt)*} {{$f0:ident, $($l:tt)*} $($f:tt)*} $($generic:tt)*) => {
48        paste! {mk_is_state_trait!{
49                $lts {$($finished)* [<Has $f0:camel Setter>] <$($l)*> +} {$($f)*} $($generic)*
50                // $lts {$($finished)* [<Has $f0:camel Setter>] <$($l)* $($generic)*> +} {$($f)*} $($generic)*
51        }}
52    };
53    ({$($glts:lifetime,)*} {$($finished:tt)*} {} $($generic:tt)*) => {
54        pub trait IsState<$($glts,)*> = $($finished)*;
55    };
56}
57macro_rules! mk {
58    (struct $state:ident<$($glts:lifetime),*> {$($field:ident : {$($lts:lifetime),*} $field_type:ty),*$(,)?}) => {
59        mk!(@$state {} {$($field)*} {$($field: {$($lts),*} {$field_type},)*});
60        mk_is_state_trait!({$($glts,)*} {} {$({$field, $($lts,)*})*} $([<$field:camel>],)*);
61    };
62    (@$state:ident {$($acc:tt)*} $fields:tt {
63        $field:ident : $lts:tt $field_type:tt
64        $(,$($rest:tt)*)?
65    }) => {mk!(@$state {
66        $($acc)* $fields $field: $lts $field_type,
67    } $fields {$($($rest)*)?} );};
68    (@$state:ident $body:tt $fields:tt {$(,)?}) => { mk! (@@ $state $body ); };
69    (@@$state:ident {$({$($fields:tt)*} $field:ident : {$($lts:lifetime)*} {$($field_type:tt)+},)*}) => {
70        paste! {
71            #[derive(Clone)]
72            pub struct $state<$([<$field:camel>],)*>{
73                $(pub $field: [<$field:camel>],)*
74            }
75        }
76        $(
77            macro_rules! __inner_helper {
78                ($gen:tt {$$($full_gen:tt)*} {$$($params:tt)*} $field $$($rest:tt)*) => {
79                    paste! {__inner_helper!(
80                        $gen {$$($full_gen)*[<$field:camel>],}
81                        {$$($params)*$($field_type)+<$($lts,)*>,} $$($rest)*
82                    );}
83                };
84                ({$$($gen:tt)*} {$$($full_gen:tt)*} {$$($params:tt)*} $i:ident $$($rest:tt)*) => {
85                    paste! {__inner_helper!(
86                        {$$($gen)*[<$i:camel>],} {$$($full_gen)*[<$i:camel>],}
87                        {$$($params)*[<$i:camel>],} $$($rest)*
88                    );}
89                };
90                ($gen:tt $full_gen:tt $params:tt $$(,)?) => {
91                    mk_aux!($state {$($lts)*} $field {$($field_type)+} $gen $full_gen $params {$($fields)*});
92                };
93            }
94            __inner_helper!({} {} {} $($fields)*);
95        )*
96    };
97}
98
99mod types {
100    use crate::prelude::*;
101    use rustc_middle::ty;
102    use std::{cell::RefCell, sync::Arc};
103
104    pub struct LocalContextS {
105        pub vars: HashMap<rustc_middle::thir::LocalVarId, String>,
106    }
107
108    impl Default for LocalContextS {
109        fn default() -> Self {
110            Self::new()
111        }
112    }
113
114    impl LocalContextS {
115        pub fn new() -> LocalContextS {
116            LocalContextS {
117                vars: HashMap::new(),
118            }
119        }
120    }
121
122    /// Global caches
123    #[derive(Default)]
124    pub struct GlobalCache<'tcx> {
125        /// Cache the `Span` translations.
126        pub spans: HashMap<rustc_span::Span, Span>,
127        /// Per-item cache.
128        pub per_item: HashMap<RDefId, ItemCache<'tcx>>,
129        /// A ID table session, providing fresh IDs.
130        pub id_table_session: id_table::Session,
131    }
132
133    /// Defines a mapping from types to types, for use with `TypeMap`.
134    pub struct FullDefMapper {}
135    impl TypeMapper for FullDefMapper {
136        type Value<Body: TypeMappable> = Arc<FullDef<Body>>;
137    }
138
139    /// Defines a mapping from types to types, for use with `TypeMap`.
140    pub struct PromotedFullDefsMapper {}
141    impl TypeMapper for PromotedFullDefsMapper {
142        type Value<Body: TypeMappable> = HashMap<PromotedId, Arc<FullDef<Body>>>;
143    }
144
145    /// Per-item cache
146    #[derive(Default)]
147    pub struct ItemCache<'tcx> {
148        /// The translated `DefId`.
149        pub def_id: Option<DefId>,
150        /// The translated definitions, generic in the Body kind.
151        pub full_def: TypeMap<FullDefMapper>,
152        /// The Promoted constants of this body, if any.
153        pub promoteds: TypeMap<PromotedFullDefsMapper>,
154        /// Cache the `Ty` translations.
155        pub tys: HashMap<ty::Ty<'tcx>, Ty>,
156        /// Cache the trait resolution engine for each item.
157        pub predicate_searcher: Option<crate::traits::PredicateSearcher<'tcx>>,
158        /// Cache of trait refs to resolved impl expressions.
159        pub impl_exprs: HashMap<ty::PolyTraitRef<'tcx>, crate::traits::ImplExpr>,
160    }
161
162    #[derive(Clone)]
163    pub struct Base<'tcx> {
164        pub options: Rc<hax_frontend_exporter_options::Options>,
165        pub local_ctx: Rc<RefCell<LocalContextS>>,
166        pub opt_def_id: Option<rustc_hir::def_id::DefId>,
167        pub cache: Rc<RefCell<GlobalCache<'tcx>>>,
168        pub tcx: ty::TyCtxt<'tcx>,
169        /// Rust doesn't enforce bounds on generic parameters in type
170        /// aliases. Thus, when translating type aliases, we need to
171        /// disable the resolution of implementation expressions. For
172        /// more details, please see
173        /// https://github.com/hacspec/hax/issues/707.
174        pub ty_alias_mode: bool,
175    }
176
177    impl<'tcx> Base<'tcx> {
178        pub fn new(
179            tcx: rustc_middle::ty::TyCtxt<'tcx>,
180            options: hax_frontend_exporter_options::Options,
181        ) -> Self {
182            Self {
183                tcx,
184                cache: Default::default(),
185                options: Rc::new(options),
186                // Always prefer `s.owner_id()` to `s.base().opt_def_id`.
187                // `opt_def_id` is used in `utils` for error reporting
188                opt_def_id: None,
189                local_ctx: Rc::new(RefCell::new(LocalContextS::new())),
190                ty_alias_mode: false,
191            }
192        }
193    }
194
195    pub type MacroCalls = Rc<HashMap<Span, Span>>;
196    pub type RcThir<'tcx> = Rc<rustc_middle::thir::Thir<'tcx>>;
197    pub type RcMir<'tcx> = Rc<rustc_middle::mir::Body<'tcx>>;
198    pub type UnitBinder<'tcx> = rustc_middle::ty::Binder<'tcx, ()>;
199}
200
201mk!(
202    struct State<'tcx> {
203        base: {'tcx} types::Base,
204        thir: {'tcx} types::RcThir,
205        mir: {'tcx} types::RcMir,
206        owner_id: {} rustc_hir::def_id::DefId,
207        binder: {'tcx} types::UnitBinder,
208    }
209);
210
211pub use self::types::*;
212
213pub type StateWithBase<'tcx> = State<Base<'tcx>, (), (), (), ()>;
214pub type StateWithOwner<'tcx> = State<Base<'tcx>, (), (), rustc_hir::def_id::DefId, ()>;
215pub type StateWithBinder<'tcx> =
216    State<Base<'tcx>, (), (), rustc_hir::def_id::DefId, types::UnitBinder<'tcx>>;
217pub type StateWithThir<'tcx> =
218    State<Base<'tcx>, types::RcThir<'tcx>, (), rustc_hir::def_id::DefId, ()>;
219pub type StateWithMir<'tcx> =
220    State<Base<'tcx>, (), types::RcMir<'tcx>, rustc_hir::def_id::DefId, ()>;
221
222impl<'tcx> StateWithBase<'tcx> {
223    pub fn new(
224        tcx: rustc_middle::ty::TyCtxt<'tcx>,
225        options: hax_frontend_exporter_options::Options,
226    ) -> Self {
227        Self {
228            thir: (),
229            mir: (),
230            owner_id: (),
231            binder: (),
232            base: Base::new(tcx, options),
233        }
234    }
235}
236
237impl<'tcx> StateWithOwner<'tcx> {
238    pub fn new_from_state_and_id<S: BaseState<'tcx>>(s: &S, id: rustc_hir::def_id::DefId) -> Self {
239        State {
240            thir: (),
241            mir: (),
242            owner_id: id,
243            binder: (),
244            base: s.base().clone(),
245        }
246    }
247}
248impl<'tcx> StateWithMir<'tcx> {
249    pub fn new_from_mir(
250        tcx: rustc_middle::ty::TyCtxt<'tcx>,
251        options: hax_frontend_exporter_options::Options,
252        mir: rustc_middle::mir::Body<'tcx>,
253        owner_id: rustc_hir::def_id::DefId,
254    ) -> Self {
255        Self {
256            thir: (),
257            mir: Rc::new(mir),
258            owner_id,
259            binder: (),
260            base: Base::new(tcx, options),
261        }
262    }
263}
264impl<'tcx> StateWithThir<'tcx> {
265    pub fn from_thir(
266        base: Base<'tcx>,
267        owner_id: rustc_hir::def_id::DefId,
268        thir: types::RcThir<'tcx>,
269    ) -> Self {
270        Self {
271            thir,
272            mir: (),
273            owner_id,
274            binder: (),
275            base,
276        }
277    }
278}
279
280impl<'tcx> StateWithOwner<'tcx> {
281    pub fn from_under_owner<S: UnderOwnerState<'tcx>>(s: &S) -> Self {
282        Self {
283            base: s.base(),
284            owner_id: s.owner_id(),
285            thir: (),
286            mir: (),
287            binder: (),
288        }
289    }
290}
291
292/// Updates the OnwerId in a state, making sure to override `opt_def_id` in base as well.
293pub fn with_owner_id<THIR, MIR>(
294    mut base: types::Base<'_>,
295    thir: THIR,
296    mir: MIR,
297    owner_id: rustc_hir::def_id::DefId,
298) -> State<types::Base<'_>, THIR, MIR, rustc_hir::def_id::DefId, ()> {
299    base.opt_def_id = Some(owner_id);
300    State {
301        thir,
302        owner_id,
303        base,
304        mir,
305        binder: (),
306    }
307}
308
309pub trait BaseState<'tcx> = HasBase<'tcx> + Clone + IsState<'tcx>;
310
311/// State of anything below a `owner_id`.
312pub trait UnderOwnerState<'tcx> = BaseState<'tcx> + HasOwnerId;
313
314/// State of anything below a binder.
315pub trait UnderBinderState<'tcx> = UnderOwnerState<'tcx> + HasBinder<'tcx>;
316
317/// While translating expressions, we expect to always have a THIR
318/// body and an `owner_id` in the state
319pub trait ExprState<'tcx> = UnderOwnerState<'tcx> + HasThir<'tcx>;
320
321pub trait WithGlobalCacheExt<'tcx>: BaseState<'tcx> {
322    /// Access the global cache. You must not call `sinto` within this function as this will likely
323    /// result in `BorrowMut` panics.
324    fn with_global_cache<T>(&self, f: impl FnOnce(&mut GlobalCache<'tcx>) -> T) -> T {
325        let base = self.base();
326        let mut cache = base.cache.borrow_mut();
327        f(&mut *cache)
328    }
329    /// Access the cache for a given item. You must not call `sinto` within this function as this
330    /// will likely result in `BorrowMut` panics.
331    fn with_item_cache<T>(&self, def_id: RDefId, f: impl FnOnce(&mut ItemCache<'tcx>) -> T) -> T {
332        self.with_global_cache(|cache| f(cache.per_item.entry(def_id).or_default()))
333    }
334}
335impl<'tcx, S: BaseState<'tcx>> WithGlobalCacheExt<'tcx> for S {}
336
337pub trait WithItemCacheExt<'tcx>: UnderOwnerState<'tcx> {
338    /// Access the cache for the current item. You must not call `sinto` within this function as
339    /// this will likely result in `BorrowMut` panics.
340    fn with_cache<T>(&self, f: impl FnOnce(&mut ItemCache<'tcx>) -> T) -> T {
341        self.with_item_cache(self.owner_id(), f)
342    }
343}
344impl<'tcx, S: UnderOwnerState<'tcx>> WithItemCacheExt<'tcx> for S {}
345
346impl ImplInfos {
347    fn from(base: Base<'_>, did: rustc_hir::def_id::DefId) -> Self {
348        let tcx = base.tcx;
349        let s = &with_owner_id(base, (), (), did);
350
351        Self {
352            generics: tcx.generics_of(did).sinto(s),
353            typ: tcx.type_of(did).instantiate_identity().sinto(s),
354            trait_ref: tcx
355                .impl_trait_ref(did)
356                .map(|trait_ref| trait_ref.instantiate_identity())
357                .sinto(s),
358            clauses: predicates_defined_on(tcx, did).predicates.sinto(s),
359        }
360    }
361}
362
363/// Returns a map from every implementation (`Impl`) `DefId`s to the
364/// type they implement, plus the bounds.
365pub fn impl_def_ids_to_impled_types_and_bounds<'tcx, S: BaseState<'tcx>>(
366    s: &S,
367) -> HashMap<DefId, ImplInfos> {
368    let tcx = s.base().tcx;
369
370    let def_ids: Vec<_> = s.with_global_cache(|cache| cache.per_item.keys().copied().collect());
371    let with_parents = |mut did: rustc_hir::def_id::DefId| {
372        let mut acc = vec![did];
373        while let Some(parent) = tcx.opt_parent(did) {
374            did = parent;
375            acc.push(did);
376        }
377        acc.into_iter()
378    };
379    use itertools::Itertools;
380    def_ids
381        .into_iter()
382        .flat_map(with_parents)
383        .unique()
384        .filter(|&did| {
385            // keep only DefIds that corresponds to implementations
386            matches!(
387                tcx.def_path(did).data.last(),
388                Some(rustc_hir::definitions::DisambiguatedDefPathData {
389                    data: rustc_hir::definitions::DefPathData::Impl,
390                    ..
391                })
392            )
393        })
394        .map(|did| (did.sinto(s), ImplInfos::from(s.base(), did)))
395        .collect()
396}
hax_frontend_exporter/state.rs

hax_frontend_exporter/
state.rs
