flux_middle/
lib.rs

1//! This crate contains common type definitions that are used by other crates.
2#![feature(
3    associated_type_defaults,
4    box_patterns,
5    closure_track_caller,
6    if_let_guard,
7    map_try_insert,
8    min_specialization,
9    never_type,
10    rustc_private,
11    unwrap_infallible,
12    new_range_api
13)]
14
15extern crate rustc_abi;
16extern crate rustc_ast;
17extern crate rustc_data_structures;
18extern crate rustc_errors;
19extern crate rustc_hir;
20extern crate rustc_index;
21extern crate rustc_macros;
22extern crate rustc_middle;
23extern crate rustc_serialize;
24extern crate rustc_span;
25extern crate rustc_type_ir;
26
27extern crate self as flux_middle;
28
29pub mod big_int;
30mod builtin_assoc_refts;
31pub mod call_graph;
32pub mod cstore;
33pub mod def_id;
34pub mod fhir;
35pub mod global_env;
36pub mod metrics;
37pub mod pretty;
38pub mod queries;
39pub mod rty;
40mod sort_of;
41
42use std::sync::LazyLock;
43
44use flux_arc_interner::List;
45use flux_macros::fluent_messages;
46pub use flux_rustc_bridge::def_id_to_string;
47use flux_rustc_bridge::{
48    mir::{LocalDecls, PlaceElem},
49    ty::{self, GenericArgsExt},
50};
51use flux_syntax::surface::{self, NodeId};
52use global_env::GlobalEnv;
53use liquid_fixpoint::ThyFunc;
54use queries::QueryResult;
55use rty::VariantIdx;
56use rustc_abi::FieldIdx;
57use rustc_data_structures::{
58    fx::FxIndexMap,
59    unord::{UnordMap, UnordSet},
60};
61use rustc_hir::OwnerId;
62use rustc_macros::{Decodable, Encodable, extension};
63use rustc_middle::ty::TyCtxt;
64use rustc_span::{
65    Symbol,
66    def_id::{DefId, LocalDefId},
67    symbol::Ident,
68};
69
70fluent_messages! { "../locales/en-US.ftl" }
71
72#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, Encodable, Decodable)]
73pub enum PanicSpec {
74    WillNotPanic,
75    MightPanic(PanicReason),
76}
77
78#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
79pub enum PanicReason {
80    Transitive,
81    UnresolvedCall(DefId),
82    DynamicDispatch,
83    SynthesizedPanic,
84    NotInCallGraph,
85    NoMIRAvailable,
86}
87
88pub struct TheoryFunc {
89    pub name: Symbol,
90    pub sort: rty::PolyFuncSort,
91    pub itf: liquid_fixpoint::ThyFunc,
92}
93
94pub static THEORY_FUNCS: LazyLock<UnordMap<liquid_fixpoint::ThyFunc, TheoryFunc>> =
95    LazyLock::new(|| {
96        use rty::{BvSize, Sort::*};
97        liquid_fixpoint::ThyFunc::ALL
98            .into_iter()
99            .filter_map(|func| {
100                let func = TheoryFunc {
101                    name: Symbol::intern(name_of_thy_func(func)?),
102                    itf: func,
103                    sort: sort_of_thy_func(func)?,
104                };
105                Some(func)
106            })
107            .chain([
108                // we can't express these as function types so we add special case
109                TheoryFunc {
110                    name: Symbol::intern("bv_zero_extend_32_to_64"),
111                    itf: liquid_fixpoint::ThyFunc::BvZeroExtend(32),
112                    sort: rty::PolyFuncSort::new(
113                        List::empty(),
114                        rty::FuncSort::new(
115                            vec![BitVec(BvSize::Fixed(32))],
116                            BitVec(BvSize::Fixed(64)),
117                        ),
118                    ),
119                },
120                TheoryFunc {
121                    name: Symbol::intern("bv_sign_extend_32_to_64"),
122                    itf: liquid_fixpoint::ThyFunc::BvSignExtend(32),
123                    sort: rty::PolyFuncSort::new(
124                        List::empty(),
125                        rty::FuncSort::new(
126                            vec![BitVec(BvSize::Fixed(32))],
127                            BitVec(BvSize::Fixed(64)),
128                        ),
129                    ),
130                },
131            ])
132            .map(|func| (func.itf, func))
133            .collect()
134    });
135
136pub fn name_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<&'static str> {
137    let name = match func {
138        ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
139        ThyFunc::StrLen => "str_len",
140        ThyFunc::StrConcat => "str_concat",
141        ThyFunc::StrPrefixOf => "str_prefix_of",
142        ThyFunc::StrSuffixOf => "str_suffix_of",
143        ThyFunc::StrContains => "str_contains",
144        ThyFunc::IntToBv8 => "bv_int_to_bv8",
145        ThyFunc::Bv8ToInt => "bv_bv8_to_int",
146        ThyFunc::IntToBv32 => "bv_int_to_bv32",
147        ThyFunc::Bv32ToInt => "bv_bv32_to_int",
148        ThyFunc::IntToBv64 => "bv_int_to_bv64",
149        ThyFunc::Bv64ToInt => "bv_bv64_to_int",
150        ThyFunc::BvUge => "bv_uge",
151        ThyFunc::BvSge => "bv_sge",
152        ThyFunc::BvUdiv => "bv_udiv",
153        ThyFunc::BvSdiv => "bv_sdiv",
154        ThyFunc::BvSrem => "bv_srem",
155        ThyFunc::BvUrem => "bv_urem",
156        ThyFunc::BvLshr => "bv_lshr",
157        ThyFunc::BvAshr => "bv_ashr",
158        ThyFunc::BvAnd => "bv_and",
159        ThyFunc::BvOr => "bv_or",
160        ThyFunc::BvXor => "bv_xor",
161        ThyFunc::BvNot => "bv_not",
162        ThyFunc::BvAdd => "bv_add",
163        ThyFunc::BvNeg => "bv_neg",
164        ThyFunc::BvSub => "bv_sub",
165        ThyFunc::BvMul => "bv_mul",
166        ThyFunc::BvShl => "bv_shl",
167        ThyFunc::BvUle => "bv_ule",
168        ThyFunc::BvSle => "bv_sle",
169        ThyFunc::BvUgt => "bv_ugt",
170        ThyFunc::BvSgt => "bv_sgt",
171        ThyFunc::BvUlt => "bv_ult",
172        ThyFunc::BvSlt => "bv_slt",
173        ThyFunc::SetEmpty => "set_empty",
174        ThyFunc::SetSng => "set_singleton",
175        ThyFunc::SetCup => "set_union",
176        ThyFunc::SetCap => "set_intersection",
177        ThyFunc::SetDif => "set_difference",
178        ThyFunc::SetSub => "set_subset",
179        ThyFunc::SetMem => "set_is_in",
180        ThyFunc::MapDefault => "map_default",
181        ThyFunc::MapSelect => "map_select",
182        ThyFunc::MapStore => "map_store",
183    };
184    Some(name)
185}
186
187fn sort_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<rty::PolyFuncSort> {
188    use rty::{
189        BvSize, ParamSort,
190        Sort::{self, *},
191        SortCtor::*,
192        SortParamKind,
193    };
194    let param0 = ParamSort::from_u32(0);
195    let param1 = ParamSort::from_u32(1);
196    let bv_param0 = BvSize::Param(ParamSort::from_u32(0));
197
198    let sort = match func {
199        ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
200        ThyFunc::StrLen => {
201            // str -> int
202            rty::PolyFuncSort::new(List::empty(), rty::FuncSort::new(vec![rty::Sort::Str], Int))
203        }
204        ThyFunc::StrConcat => {
205            // (str, str) -> str
206            rty::PolyFuncSort::new(
207                List::empty(),
208                rty::FuncSort::new(vec![rty::Sort::Str, rty::Sort::Str], rty::Sort::Str),
209            )
210        }
211        ThyFunc::StrPrefixOf | ThyFunc::StrSuffixOf | ThyFunc::StrContains => {
212            // (str, str) -> bool
213            rty::PolyFuncSort::new(
214                List::empty(),
215                rty::FuncSort::new(vec![rty::Sort::Str, rty::Sort::Str], Bool),
216            )
217        }
218        ThyFunc::IntToBv8 => {
219            // int -> BitVec<8>
220            rty::PolyFuncSort::new(
221                List::empty(),
222                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(8))),
223            )
224        }
225        ThyFunc::Bv8ToInt => {
226            // BitVec<8> -> int
227            rty::PolyFuncSort::new(
228                List::empty(),
229                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(8))], Int),
230            )
231        }
232        ThyFunc::IntToBv32 => {
233            // int -> BitVec<32>
234            rty::PolyFuncSort::new(
235                List::empty(),
236                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(32))),
237            )
238        }
239        ThyFunc::Bv32ToInt => {
240            // BitVec<32> -> int
241            rty::PolyFuncSort::new(
242                List::empty(),
243                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(32))], Int),
244            )
245        }
246        ThyFunc::IntToBv64 => {
247            // int -> BitVec<64>
248            rty::PolyFuncSort::new(
249                List::empty(),
250                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(64))),
251            )
252        }
253        ThyFunc::Bv64ToInt => {
254            // BitVec<64> -> int
255            rty::PolyFuncSort::new(
256                List::empty(),
257                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(64))], Int),
258            )
259        }
260        ThyFunc::BvUdiv
261        | ThyFunc::BvSdiv
262        | ThyFunc::BvSrem
263        | ThyFunc::BvUrem
264        | ThyFunc::BvLshr
265        | ThyFunc::BvAshr
266        | ThyFunc::BvAnd
267        | ThyFunc::BvOr
268        | ThyFunc::BvXor
269        | ThyFunc::BvAdd
270        | ThyFunc::BvSub
271        | ThyFunc::BvMul
272        | ThyFunc::BvShl => {
273            // ∀s. (BitVec<s>, BitVec<s>) -> BitVec<s>
274            rty::PolyFuncSort::new(
275                List::singleton(SortParamKind::BvSize),
276                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], BitVec(bv_param0)),
277            )
278        }
279        ThyFunc::BvNot | ThyFunc::BvNeg => {
280            // ∀s. BitVec<s> -> BitVec<s>
281            rty::PolyFuncSort::new(
282                List::singleton(SortParamKind::BvSize),
283                rty::FuncSort::new(vec![BitVec(bv_param0)], BitVec(bv_param0)),
284            )
285        }
286        ThyFunc::BvUgt
287        | ThyFunc::BvSgt
288        | ThyFunc::BvUlt
289        | ThyFunc::BvSlt
290        | ThyFunc::BvSle
291        | ThyFunc::BvUge
292        | ThyFunc::BvSge
293        | ThyFunc::BvUle => {
294            // ∀s. (BitVec<s>, BitVec<s>) -> bool
295            rty::PolyFuncSort::new(
296                List::singleton(SortParamKind::BvSize),
297                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
298            )
299        }
300        ThyFunc::SetEmpty => {
301            // ∀s. int -> Set<S> why does this take an int?
302            rty::PolyFuncSort::new(
303                List::singleton(SortParamKind::Sort),
304                rty::FuncSort::new(vec![Int], Sort::app(Set, List::singleton(Var(param0)))),
305            )
306        }
307        ThyFunc::SetSng => {
308            // ∀s. s -> Set<S>
309            rty::PolyFuncSort::new(
310                List::singleton(SortParamKind::Sort),
311                rty::FuncSort::new(vec![Var(param0)], Sort::app(Set, List::singleton(Var(param0)))),
312            )
313        }
314        ThyFunc::SetCup | ThyFunc::SetCap | ThyFunc::SetDif => {
315            // ∀s. (Set<S>, Set<S>) -> Set<S>
316            rty::PolyFuncSort::new(
317                List::singleton(SortParamKind::Sort),
318                rty::FuncSort::new(
319                    vec![
320                        Sort::app(Set, List::singleton(Var(param0))),
321                        Sort::app(Set, List::singleton(Var(param0))),
322                    ],
323                    Sort::app(Set, List::singleton(Var(param0))),
324                ),
325            )
326        }
327        ThyFunc::SetMem => {
328            // ∀s. (s, Set<S>) -> bool
329            rty::PolyFuncSort::new(
330                List::singleton(SortParamKind::Sort),
331                rty::FuncSort::new(
332                    vec![Var(param0), Sort::app(Set, List::singleton(Var(param0)))],
333                    Bool,
334                ),
335            )
336        }
337        ThyFunc::SetSub => {
338            // ∀s. (Set<s>, Set<s>) -> bool
339            rty::PolyFuncSort::new(
340                List::singleton(SortParamKind::Sort),
341                rty::FuncSort::new(
342                    vec![
343                        Sort::app(Set, List::singleton(Var(param0))),
344                        Sort::app(Set, List::singleton(Var(param0))),
345                    ],
346                    Bool,
347                ),
348            )
349        }
350
351        ThyFunc::MapDefault => {
352            // ∀k,v. v -> Map<k,v>
353            rty::PolyFuncSort::new(
354                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
355                rty::FuncSort::new(
356                    vec![Var(param1)],
357                    Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
358                ),
359            )
360        }
361        ThyFunc::MapSelect => {
362            // ∀k,v. (Map<k,v>, k) -> v
363            rty::PolyFuncSort::new(
364                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
365                rty::FuncSort::new(
366                    vec![Sort::app(Map, List::from_arr([Var(param0), Var(param1)])), Var(param0)],
367                    Var(param1),
368                ),
369            )
370        }
371        ThyFunc::MapStore => {
372            // ∀k,v. (Map<k,v>, k, v) -> Map<k, v>
373            rty::PolyFuncSort::new(
374                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
375                rty::FuncSort::new(
376                    vec![
377                        Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
378                        Var(param0),
379                        Var(param1),
380                    ],
381                    Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
382                ),
383            )
384        }
385    };
386    Some(sort)
387}
388
389#[derive(Default)]
390pub struct Specs {
391    items: UnordMap<OwnerId, surface::Item>,
392    trait_items: UnordMap<OwnerId, surface::TraitItemFn>,
393    impl_items: UnordMap<OwnerId, surface::ImplItemFn>,
394    pub flux_items_by_parent: FxIndexMap<OwnerId, Vec<surface::FluxItem>>,
395    /// Set of dummy items generated by the extern spec macro we must completely ignore. This is
396    /// not the same as [ignored items] because, for ignored items, we still need to return errors
397    /// for queries and handle them gracefully in order to report them at the use it.
398    ///
399    /// If an item is in this set, all its descendants are also consider dummy (but they may not be
400    /// in the set).
401    ///
402    /// [ignored items]: Specs::ignores
403    dummy_extern: UnordSet<LocalDefId>,
404    extern_id_to_local_id: UnordMap<DefId, LocalDefId>,
405    local_id_to_extern_id: UnordMap<LocalDefId, DefId>,
406}
407
408impl Specs {
409    pub fn insert_extern_spec_id_mapping(
410        &mut self,
411        local_id: LocalDefId,
412        extern_id: DefId,
413    ) -> Result<(), ExternSpecMappingErr> {
414        #[expect(
415            clippy::disallowed_methods,
416            reason = "we are inserting the extern spec mapping and we want to ensure it doesn't point to a local item"
417        )]
418        if let Some(local) = extern_id.as_local() {
419            return Err(ExternSpecMappingErr::IsLocal(local));
420        }
421        if let Err(err) = self.extern_id_to_local_id.try_insert(extern_id, local_id) {
422            return Err(ExternSpecMappingErr::Dup(*err.entry.get()));
423        }
424        self.local_id_to_extern_id.insert(local_id, extern_id);
425        Ok(())
426    }
427
428    pub fn insert_dummy(&mut self, def_id: LocalDefId) {
429        self.dummy_extern.insert(def_id);
430    }
431
432    pub fn get_item(&self, owner_id: OwnerId) -> Option<&surface::Item> {
433        self.items.get(&owner_id)
434    }
435
436    pub fn insert_item(&mut self, owner_id: OwnerId, item: surface::Item) -> Option<surface::Item> {
437        if let Some(old) = self.items.insert(owner_id, item) {
438            return Some(old);
439        }
440        None
441    }
442
443    pub fn get_trait_item(&self, owner_id: OwnerId) -> Option<&surface::TraitItemFn> {
444        self.trait_items.get(&owner_id)
445    }
446
447    pub fn insert_trait_item(
448        &mut self,
449        owner_id: OwnerId,
450        trait_item: surface::TraitItemFn,
451    ) -> Option<surface::TraitItemFn> {
452        if let Some(old) = self.trait_items.insert(owner_id, trait_item) {
453            return Some(old);
454        }
455        None
456    }
457
458    pub fn get_impl_item(&self, owner_id: OwnerId) -> Option<&surface::ImplItemFn> {
459        self.impl_items.get(&owner_id)
460    }
461
462    pub fn insert_impl_item(
463        &mut self,
464        owner_id: OwnerId,
465        impl_item: surface::ImplItemFn,
466    ) -> Option<surface::ImplItemFn> {
467        if let Some(old) = self.impl_items.insert(owner_id, impl_item) {
468            return Some(old);
469        }
470        None
471    }
472}
473
474/// Represents errors that can occur when inserting a mapping between a `LocalDefId` and a `DefId`
475/// for an extern spec.
476pub enum ExternSpecMappingErr {
477    /// Indicates that the [`DefId`] we are trying to add extern specs to is actually local. Returns
478    /// the [`DefId`] as a [`LocalDefId`].
479    IsLocal(LocalDefId),
480
481    /// Indicates that there is an existing extern spec for the given extern id. Returns the existing
482    /// `LocalDefId` that maps to the extern id.
483    ///
484    /// NOTE: This currently only considers extern specs defined in the local crate. There could still
485    /// be duplicates if an extern spec is imported from an external crate. In such cases, the local
486    /// extern spec takes precedence. Probably, we should at least warn about this, but it's a bit
487    /// tricky because we need to look at the crate metadata which we don't have handy when
488    /// collecting specs.
489    Dup(LocalDefId),
490}
491
492#[derive(Default)]
493pub struct ResolverOutput {
494    pub path_res_map: UnordMap<NodeId, fhir::PartialRes>,
495    /// Resolution of explicitly and implicitly scoped parameters. The [`fhir::ParamId`] is unique
496    /// per item. The [`NodeId`] used as the key corresponds to the node introducing the parameter.
497    /// When explicit, this is the id of the [`surface::GenericArg`] or [`surface::RefineParam`],
498    /// when implicit, this is the id of the [`surface::RefineArg::Bind`] or [`surface::FnInput`].
499    pub param_res_map: UnordMap<NodeId, (fhir::ParamId, fhir::ParamKind)>,
500    /// List of implicitly scoped params defined in a scope. The [`NodeId`] used as key is the id of
501    /// the node introducing the scope, e.g., [`surface::FnSig`], [`surface::FnOutput`], or
502    /// [`surface::VariantDef`]. The [`NodeId`]s in the vectors are keys in [`Self::param_res_map`].
503    pub implicit_params: UnordMap<NodeId, Vec<(Ident, NodeId)>>,
504    pub sort_path_res_map: UnordMap<NodeId, fhir::SortRes>,
505    pub expr_path_res_map: UnordMap<NodeId, fhir::PartialRes<fhir::ParamId>>,
506    /// The resolved list of local qualifiers per function.
507    /// The [`NodeId`] corresponds to the [`surface::FnSpec`].
508    pub qualifier_res_map: UnordMap<NodeId, Vec<def_id::FluxLocalDefId>>,
509    /// The resolved list of local reveals per function
510    /// The [`NodeId`] corresponds to the [`surface::FnSpec`].
511    pub reveal_res_map: UnordMap<NodeId, Vec<def_id::FluxDefId>>,
512    /// The resolved type param `DefId`s for `#[assume_parametric(...)]` per function.
513    /// The [`NodeId`] corresponds to the surface item's `node_id`.
514    pub parametric_param_res_map: UnordMap<NodeId, Vec<DefId>>,
515}
516
517#[extension(pub trait PlaceExt)]
518impl flux_rustc_bridge::mir::Place {
519    fn ty(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<PlaceTy> {
520        self.projection
521            .iter()
522            .try_fold(PlaceTy::from_ty(local_decls[self.local].ty.clone()), |place_ty, elem| {
523                place_ty.projection_ty(genv, *elem)
524            })
525    }
526
527    fn behind_raw_ptr(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<bool> {
528        let mut place_ty = PlaceTy::from_ty(local_decls[self.local].ty.clone());
529        for elem in &self.projection {
530            if let (PlaceElem::Deref, ty::TyKind::RawPtr(..)) = (elem, place_ty.ty.kind()) {
531                return Ok(true);
532            }
533            place_ty = place_ty.projection_ty(genv, *elem)?;
534        }
535        Ok(false)
536    }
537}
538
539#[derive(Debug)]
540pub struct PlaceTy {
541    pub ty: ty::Ty,
542    /// Downcast to a particular variant of an enum or a generator, if included.
543    pub variant_index: Option<VariantIdx>,
544}
545
546impl PlaceTy {
547    fn from_ty(ty: ty::Ty) -> PlaceTy {
548        PlaceTy { ty, variant_index: None }
549    }
550
551    fn projection_ty(&self, genv: GlobalEnv, elem: PlaceElem) -> QueryResult<PlaceTy> {
552        if self.variant_index.is_some() && !matches!(elem, PlaceElem::Field(..)) {
553            Err(query_bug!("cannot use non field projection on downcasted place"))?;
554        }
555        let place_ty = match elem {
556            PlaceElem::Deref => PlaceTy::from_ty(self.ty.deref()),
557            PlaceElem::Field(fld) => PlaceTy::from_ty(self.field_ty(genv, fld)?),
558            PlaceElem::Downcast(_, variant_idx) => {
559                PlaceTy { ty: self.ty.clone(), variant_index: Some(variant_idx) }
560            }
561            PlaceElem::Index(_) | PlaceElem::ConstantIndex { .. } => {
562                if let ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) = self.ty.kind() {
563                    PlaceTy::from_ty(ty.clone())
564                } else {
565                    return Err(query_bug!("cannot use non field projection on downcasted place"));
566                }
567            }
568        };
569        Ok(place_ty)
570    }
571
572    fn field_ty(&self, genv: GlobalEnv, f: FieldIdx) -> QueryResult<ty::Ty> {
573        match self.ty.kind() {
574            ty::TyKind::Adt(adt_def, args) => {
575                let variant_def = match self.variant_index {
576                    None => adt_def.non_enum_variant(),
577                    Some(variant_index) => {
578                        assert!(adt_def.is_enum());
579                        adt_def.variant(variant_index)
580                    }
581                };
582                let field_def = &variant_def.fields[f];
583                let ty = genv.lower_type_of(field_def.did)?;
584                Ok(ty.subst(args))
585            }
586            ty::TyKind::Tuple(tys) => Ok(tys[f.index()].clone()),
587            ty::TyKind::Closure(_, args) => Ok(args.as_closure().upvar_tys()[f.index()].clone()),
588            _ => Err(query_bug!("extracting field of non-tuple non-adt non-closure: {self:?}")),
589        }
590    }
591}
592
593/// The different reasons we issue fixpoint queries. This is used to dissambiguate queries that
594/// are issued for the same item.
595///
596/// NOTE: This is defined here because it's also used in [`metrics`]
597#[derive(Debug, Hash, Clone, Copy)]
598pub enum FixpointQueryKind {
599    /// Query issued when checking an impl method is a subtype of the trait
600    Impl,
601    /// Query issued to check the body of a function
602    Body,
603    /// Query issued to check an (enum) invariant is implied by the type definition
604    Invariant,
605}
606
607impl FixpointQueryKind {
608    pub fn ext(self) -> &'static str {
609        match self {
610            FixpointQueryKind::Impl => "sub.fluxc",
611            FixpointQueryKind::Body => "fluxc",
612            FixpointQueryKind::Invariant => "fluxc",
613        }
614    }
615
616    /// A string that uniquely identifies a query given an item `DefId`
617    pub fn task_key(self, tcx: TyCtxt, def_id: DefId) -> String {
618        format!("{}###{:?}", tcx.def_path_str(def_id), self)
619    }
620
621    /// Returns `true` if the fixpoint query kind is [`Body`].
622    ///
623    /// [`Body`]: FixpointQueryKind::Body
624    #[must_use]
625    pub fn is_body(&self) -> bool {
626        matches!(self, Self::Body)
627    }
628}
flux_middle/lib.rs

flux_middle/
lib.rs
