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},
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                // Sized
31                let sized_id = tcx.require_lang_item(LangItem::Sized, DUMMY_SP);
32                map.insert(
33                    sized_id,
34                    AssocRefinements {
35                        items: List::from_arr([AssocReft::new(
36                            FluxDefId::new(def_id, sym::size_of),
37                            false,
38                            tcx.def_span(sized_id),
39                        )]),
40                    },
41                );
42                map
43            })
44            .get(&def_id)
45            .cloned()
46    }
47
48    #[allow(
49        clippy::disallowed_methods,
50        reason = "this file is the source of truth for builtin assoc refts def ids"
51    )]
52    pub fn builtin_assoc_reft_sort(
53        self,
54        assoc_id: FluxDefId,
55    ) -> Option<rty::EarlyBinder<rty::FuncSort>> {
56        static BUILTIN: OnceLock<UnordMap<FluxDefId, rty::FuncSort>> = OnceLock::new();
57
58        BUILTIN
59            .get_or_init(|| {
60                let tcx = self.tcx();
61
62                let mut map = UnordMap::default();
63
64                // Sized
65                let sized_id = tcx.require_lang_item(LangItem::Sized, DUMMY_SP);
66                map.insert(
67                    FluxDefId::new(sized_id, sym::size_of),
68                    rty::FuncSort::new(vec![], rty::Sort::Int),
69                );
70                map
71            })
72            .get(&assoc_id)
73            .cloned()
74            .map(rty::EarlyBinder)
75    }
76
77    pub fn builtin_assoc_reft_body(
78        self,
79        typing_env: rustc_middle::ty::TypingEnv<'tcx>,
80        alias_reft: &AliasReft,
81    ) -> rty::Lambda {
82        let tcx = self.tcx();
83
84        if tcx.is_lang_item(alias_reft.assoc_id.parent(), LangItem::Sized)
85            && alias_reft.assoc_id.name() == sym::size_of
86        {
87            let self_ty = alias_reft.to_rustc_trait_ref(tcx).self_ty();
88            let size = tcx
89                .layout_of(typing_env.as_query_input(self_ty))
90                .unwrap()
91                .size
92                .bytes();
93            let body = rty::Expr::constant(rty::Constant::from(size));
94            rty::Lambda::bind_with_vars(body, List::empty(), rty::Sort::Int)
95        } else {
96            bug!("invalid builtin assoc reft {:?}", alias_reft.assoc_id)
97        }
98    }
99}
flux_middle/builtin_assoc_refts.rs

flux_middle/
builtin_assoc_refts.rs
