flux_middle/
builtin_assoc_refts.rs

1use std::sync::OnceLock;
2
3use flux_arc_interner::List;
4use flux_common::bug;
5use flux_syntax::symbols::sym;
6use rustc_data_structures::unord::UnordMap;
7use rustc_hir::{LangItem, def_id::DefId};
8use rustc_span::DUMMY_SP;
9
10use crate::{
11    def_id::FluxDefId,
12    global_env::GlobalEnv,
13    rty::{self, AliasReft, AssocRefinements, AssocReft, BaseTy},
14};
15
16impl<'tcx> GlobalEnv<'_, 'tcx> {
17    #[allow(
18        clippy::disallowed_methods,
19        reason = "this file is the source of truth for builtin assoc refts def ids"
20    )]
21    pub fn builtin_assoc_refts(self, def_id: DefId) -> Option<AssocRefinements> {
22        static BUILTIN: OnceLock<UnordMap<DefId, AssocRefinements>> = OnceLock::new();
23
24        BUILTIN
25            .get_or_init(|| {
26                let tcx = self.tcx();
27
28                let mut map = UnordMap::default();
29
30                // FnOnce
31                let fn_once_id = tcx.require_lang_item(LangItem::FnOnce, DUMMY_SP);
32                map.insert(
33                    fn_once_id,
34                    AssocRefinements {
35                        items: List::from_arr([AssocReft::new(
36                            FluxDefId::new(fn_once_id, sym::no_panic),
37                            false,
38                            tcx.def_span(fn_once_id),
39                        )]),
40                    },
41                );
42
43                // Sized
44                let sized_id = tcx.require_lang_item(LangItem::Sized, DUMMY_SP);
45                map.insert(
46                    sized_id,
47                    AssocRefinements {
48                        items: List::from_arr([
49                            AssocReft::new(
50                                FluxDefId::new(def_id, sym::size_of),
51                                false,
52                                tcx.def_span(sized_id),
53                            ),
54                            AssocReft::new(
55                                FluxDefId::new(def_id, sym::align_of),
56                                false,
57                                tcx.def_span(sized_id),
58                            ),
59                        ]),
60                    },
61                );
62                map
63            })
64            .get(&def_id)
65            .cloned()
66    }
67
68    #[allow(
69        clippy::disallowed_methods,
70        reason = "this file is the source of truth for builtin assoc refts def ids"
71    )]
72    pub fn builtin_assoc_reft_sort(
73        self,
74        assoc_id: FluxDefId,
75    ) -> Option<rty::EarlyBinder<rty::FuncSort>> {
76        static BUILTIN: OnceLock<UnordMap<FluxDefId, rty::FuncSort>> = OnceLock::new();
77
78        BUILTIN
79            .get_or_init(|| {
80                let tcx = self.tcx();
81
82                let mut map = UnordMap::default();
83
84                // FnOnce
85                let fn_once_id = tcx.require_lang_item(LangItem::FnOnce, DUMMY_SP);
86                map.insert(
87                    FluxDefId::new(fn_once_id, sym::no_panic),
88                    rty::FuncSort::new(vec![], rty::Sort::Bool),
89                );
90
91                // Sized
92                let sized_id = tcx.require_lang_item(LangItem::Sized, DUMMY_SP);
93                map.insert(
94                    FluxDefId::new(sized_id, sym::size_of),
95                    rty::FuncSort::new(vec![], rty::Sort::Int),
96                );
97                map.insert(
98                    FluxDefId::new(sized_id, sym::align_of),
99                    rty::FuncSort::new(vec![], rty::Sort::Int),
100                );
101                map
102            })
103            .get(&assoc_id)
104            .cloned()
105            .map(rty::EarlyBinder)
106    }
107
108    pub fn builtin_assoc_reft_body(
109        self,
110        typing_env: rustc_middle::ty::TypingEnv<'tcx>,
111        alias_reft: &AliasReft,
112    ) -> rty::Lambda {
113        let tcx = self.tcx();
114
115        if tcx.is_lang_item(alias_reft.assoc_id.parent(), LangItem::Sized) {
116            let self_ty = alias_reft.to_rustc_trait_ref(tcx).self_ty();
117            let layout = tcx.layout_of(typing_env.as_query_input(self_ty)).unwrap();
118            let body = match alias_reft.assoc_id.name() {
119                sym::size_of => rty::Expr::constant(rty::Constant::from(layout.size.bytes())),
120                sym::align_of => rty::Expr::constant(rty::Constant::from(layout.align.abi.bytes())),
121                _ => bug!("invalid builtin assoc reft {:?}", alias_reft.assoc_id),
122            };
123            rty::Lambda::bind_with_vars(body, List::empty(), rty::Sort::Int)
124        } else if tcx.is_lang_item(alias_reft.assoc_id.parent(), LangItem::FnOnce)
125            && alias_reft.assoc_id.name() == sym::no_panic
126        {
127            let self_ty = alias_reft.self_ty();
128            let body = match self_ty.as_bty_skipping_binder() {
129                BaseTy::Closure(_, _, _, no_panic) => {
130                    if *no_panic {
131                        rty::Expr::tt()
132                    } else {
133                        rty::Expr::ff()
134                    }
135                }
136                _ => rty::Expr::ff(),
137            };
138            rty::Lambda::bind_with_vars(body, List::empty(), rty::Sort::Bool)
139        } else {
140            bug!("invalid builtin assoc reft {:?}", alias_reft.assoc_id)
141        }
142    }
143}
flux_middle/builtin_assoc_refts.rs

flux_middle/
builtin_assoc_refts.rs
