flux_middle/
cstore.rs

1use std::rc::Rc;
2
3use rustc_data_structures::unord::{UnordMap, UnordSet};
4use rustc_hir::def_id::CrateNum;
5use rustc_span::{Span, def_id::DefId};
6
7use crate::{PanicSpec, call_graph::NodeKey, def_id::FluxDefId, fhir, queries::QueryResult, rty};
8
9pub type OptResult<T> = Option<QueryResult<T>>;
10
11pub trait CrateStore<'tcx> {
12    fn fn_sig(&self, def_id: DefId) -> OptResult<rty::EarlyBinder<rty::PolyFnSig>>;
13    fn adt_def(&self, def_id: DefId) -> OptResult<rty::AdtDef>;
14    fn invariants_of(&self, def_id: DefId) -> Option<rty::EarlyBinder<rty::List<rty::Invariant>>>;
15    fn adt_sort_def(&self, def_id: DefId) -> OptResult<rty::AdtSortDef>;
16    fn generics_of(&self, def_id: DefId) -> OptResult<rty::Generics>;
17    fn refinement_generics_of(
18        &self,
19        def_id: DefId,
20    ) -> OptResult<rty::EarlyBinder<rty::RefinementGenerics>>;
21    fn item_bounds(&self, def_id: DefId) -> OptResult<rty::EarlyBinder<rty::Clauses>>;
22    fn predicates_of(&self, def_id: DefId) -> OptResult<rty::EarlyBinder<rty::GenericPredicates>>;
23    fn assoc_refinements_of(&self, def_id: DefId) -> OptResult<rty::AssocRefinements>;
24    fn constant_info(&self, def_id: DefId) -> OptResult<rty::ConstantInfo>;
25    fn static_info(&self, def_id: DefId) -> OptResult<rty::Ty>;
26    fn assoc_refinements_def(&self, key: FluxDefId) -> OptResult<rty::EarlyBinder<rty::Lambda>>;
27    fn default_assoc_refinements_def(
28        &self,
29        key: FluxDefId,
30    ) -> OptResult<Option<rty::EarlyBinder<rty::Lambda>>>;
31    fn sort_of_assoc_reft(&self, key: FluxDefId) -> OptResult<rty::EarlyBinder<rty::FuncSort>>;
32    fn variants_of(
33        &self,
34        def_id: DefId,
35    ) -> OptResult<rty::Opaqueness<rty::EarlyBinder<rty::PolyVariants>>>;
36    fn type_of(&self, def_id: DefId) -> OptResult<rty::EarlyBinder<rty::TyOrCtor>>;
37    fn spec_funcs(&self, krate: CrateNum) -> Rc<rty::SpecFuncs>;
38    fn flux_module_children(&self, def_id: DefId) -> Option<&[fhir::FluxModChild]>;
39    fn func_sort(&self, def_id: FluxDefId) -> Option<rty::PolyFuncSort>;
40    fn func_span(&self, def_id: FluxDefId) -> Option<rustc_span::Span>;
41    fn sort_decl_param_count(&self, def_id: FluxDefId) -> Option<usize>;
42    fn no_panic(&self, def_id: DefId) -> Option<bool>;
43    fn assume_parametric_params(&self, def_id: DefId) -> Option<UnordSet<u32>>;
44    fn spec_attr_span(&self, def_id: DefId) -> Option<Span>;
45    fn inferred_no_panic(&self, krate: CrateNum) -> Rc<UnordMap<NodeKey<'tcx>, PanicSpec>>;
46    fn has_crate(&self, krate: CrateNum) -> bool;
47}
48
49pub type CrateStoreDyn<'tcx> = dyn CrateStore<'tcx> + 'tcx;
flux_middle/cstore.rs

flux_middle/
cstore.rs
