flux_fhir_analysis/
lib.rs

1#![feature(rustc_private, let_chains, box_patterns, if_let_guard, once_cell_try, never_type)]
2
3extern crate rustc_abi;
4extern crate rustc_ast;
5extern crate rustc_data_structures;
6extern crate rustc_errors;
7extern crate rustc_hir;
8extern crate rustc_index;
9extern crate rustc_infer;
10extern crate rustc_middle;
11extern crate rustc_span;
12extern crate rustc_trait_selection;
13extern crate rustc_type_ir;
14
15mod conv;
16mod wf;
17
18use std::rc::Rc;
19
20use conv::{AfterSortck, ConvPhase, struct_compat};
21use flux_common::{bug, dbg, iter::IterExt, result::ResultExt};
22use flux_config as config;
23use flux_errors::Errors;
24use flux_macros::fluent_messages;
25use flux_middle::{
26    def_id::{FluxDefId, FluxId, FluxLocalDefId, MaybeExternId},
27    fhir::{
28        self, ForeignItem, ForeignItemKind, ImplItem, ImplItemKind, Item, ItemKind, TraitItem,
29        TraitItemKind,
30    },
31    global_env::GlobalEnv,
32    queries::{Providers, QueryResult},
33    query_bug,
34    rty::{
35        self, WfckResults,
36        fold::TypeFoldable,
37        refining::{self, Refiner},
38    },
39};
40use flux_rustc_bridge::lowering::Lower;
41use itertools::Itertools;
42use rustc_errors::ErrorGuaranteed;
43use rustc_hir::{
44    OwnerId,
45    def::DefKind,
46    def_id::{DefId, LOCAL_CRATE, LocalDefId},
47};
48
49fluent_messages! { "../locales/en-US.ftl" }
50
51pub fn provide(providers: &mut Providers) {
52    providers.normalized_defns = normalized_defns;
53    providers.func_sort = func_sort;
54    providers.qualifiers = qualifiers;
55    providers.adt_sort_def_of = adt_sort_def_of;
56    providers.check_wf = check_wf;
57    providers.adt_def = adt_def;
58    providers.constant_info = constant_info;
59    providers.type_of = type_of;
60    providers.variants_of = variants_of;
61    providers.fn_sig = fn_sig;
62    providers.generics_of = generics_of;
63    providers.refinement_generics_of = refinement_generics_of;
64    providers.predicates_of = predicates_of;
65    providers.assoc_refinements_of = assoc_refinements_of;
66    providers.sort_of_assoc_reft = sort_of_assoc_reft;
67    providers.assoc_refinement_body = assoc_refinement_body;
68    providers.default_assoc_refinement_body = default_assoc_refinement_body;
69    providers.item_bounds = item_bounds;
70}
71
72fn adt_sort_def_of(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::AdtSortDef> {
73    let def_id = genv.maybe_extern_id(def_id);
74    let kind = genv.map().refinement_kind(def_id.local_id())?;
75    conv::conv_adt_sort_def(genv, def_id, kind)
76}
77
78fn func_sort(genv: GlobalEnv, def_id: FluxLocalDefId) -> rty::PolyFuncSort {
79    let func = genv.map().spec_func(def_id).unwrap();
80    match conv::conv_func_decl(genv, func).emit(&genv) {
81        Ok(normalized) => normalized,
82        Err(err) => {
83            genv.sess().abort(err);
84        }
85    }
86}
87
88fn normalized_defns(genv: GlobalEnv) -> rty::NormalizedDefns {
89    match try_normalized_defns(genv) {
90        Ok(normalized) => normalized,
91        Err(err) => {
92            genv.sess().abort(err);
93        }
94    }
95}
96
97fn try_normalized_defns(genv: GlobalEnv) -> Result<rty::NormalizedDefns, ErrorGuaranteed> {
98    let mut defns = vec![];
99
100    // Collect and emit all errors
101    let mut errors = Errors::new(genv.sess());
102    for (_, item) in genv.map().flux_items() {
103        let fhir::FluxItem::Func(func) = item else { continue };
104        let Some(wfckresults) = wf::check_flux_item(genv, item).collect_err(&mut errors) else {
105            continue;
106        };
107        let Ok(defn) = conv::conv_defn(genv, func, &wfckresults).emit(&errors) else {
108            continue;
109        };
110
111        if let Some(defn) = defn {
112            defns.push((func.def_id, defn, func.hide));
113        }
114    }
115    errors.into_result()?;
116
117    let defns = rty::NormalizedDefns::new(genv, &defns)
118        .map_err(|cycle| {
119            let span = genv.map().spec_func(cycle[0]).unwrap().body.unwrap().span;
120            errors::DefinitionCycle::new(span, cycle)
121        })
122        .emit(&genv)?;
123
124    Ok(defns)
125}
126
127fn qualifiers(genv: GlobalEnv) -> QueryResult<Vec<rty::Qualifier>> {
128    genv.map()
129        .qualifiers()
130        .map(|qualifier| {
131            let wfckresults = wf::check_flux_item(genv, fhir::FluxItem::Qualifier(qualifier))?;
132            Ok(conv::conv_qualifier(genv, qualifier, &wfckresults)?.normalize(genv))
133        })
134        .try_collect()
135}
136
137fn adt_def(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::AdtDef> {
138    let def_id = genv.maybe_extern_id(def_id);
139    let item = genv.map().expect_item(def_id.local_id())?;
140    let invariants = invariants_of(genv, item)?;
141
142    let adt_def = genv.tcx().adt_def(def_id.resolved_id()).lower(genv.tcx());
143
144    let is_opaque = matches!(item.kind, fhir::ItemKind::Struct(def) if def.is_opaque());
145
146    Ok(rty::AdtDef::new(adt_def, genv.adt_sort_def_of(def_id)?, invariants, is_opaque))
147}
148
149fn constant_info(genv: GlobalEnv, local_def_id: LocalDefId) -> QueryResult<rty::ConstantInfo> {
150    let def_id = genv.maybe_extern_id(local_def_id);
151    let node = genv.map().node(def_id.local_id())?;
152    let owner = rustc_hir::OwnerId { def_id: local_def_id };
153    let Some(sort) = genv.sort_of_def_id(owner.def_id.to_def_id()).emit(&genv)? else {
154        return Ok(rty::ConstantInfo::Uninterpreted);
155    };
156    match node {
157        fhir::Node::Item(fhir::Item { kind: fhir::ItemKind::Const(Some(expr)), .. }) => {
158            // for these constants we must check and use the expression
159            let wfckresults = wf::check_constant_expr(genv, owner, expr, &sort)?;
160            conv::conv_constant_expr(genv, local_def_id.to_def_id(), expr, sort, &wfckresults)
161        }
162        fhir::Node::Item(fhir::Item { kind: fhir::ItemKind::Const(None), .. })
163        | fhir::Node::AnonConst
164        | fhir::Node::TraitItem(fhir::TraitItem { kind: fhir::TraitItemKind::Const, .. })
165        | fhir::Node::ImplItem(fhir::ImplItem { kind: fhir::ImplItemKind::Const, .. }) => {
166            // for these constants we try to evaluate if they are integral and return uninterpreted if we fail
167            conv::conv_constant(genv, local_def_id.to_def_id())
168        }
169        _ => Err(query_bug!(def_id.local_id(), "expected const item"))?,
170    }
171}
172
173fn invariants_of<'genv>(
174    genv: GlobalEnv<'genv, '_>,
175    item: &fhir::Item<'genv>,
176) -> QueryResult<Vec<rty::Invariant>> {
177    let (params, invariants) = match &item.kind {
178        fhir::ItemKind::Enum(enum_def) => (enum_def.params, enum_def.invariants),
179        fhir::ItemKind::Struct(struct_def) => (struct_def.params, struct_def.invariants),
180        _ => Err(query_bug!(item.owner_id.local_id(), "expected struct or enum"))?,
181    };
182    let wfckresults = wf::check_invariants(genv, item.owner_id, params, invariants)?;
183    AfterSortck::new(genv, &wfckresults)
184        .into_conv_ctxt()
185        .conv_invariants(item.owner_id.map(|it| it.def_id), params, invariants)
186}
187
188fn predicates_of(
189    genv: GlobalEnv,
190    def_id: LocalDefId,
191) -> QueryResult<rty::EarlyBinder<rty::GenericPredicates>> {
192    let def_id = genv.maybe_extern_id(def_id);
193    match genv.def_kind(def_id) {
194        DefKind::Impl { .. }
195        | DefKind::Struct
196        | DefKind::Enum
197        | DefKind::Union
198        | DefKind::TyAlias
199        | DefKind::AssocFn
200        | DefKind::AssocTy
201        | DefKind::Trait
202        | DefKind::Fn => {
203            let did = def_id.local_id();
204            let generics = genv
205                .map()
206                .get_generics(did)?
207                .ok_or_else(|| query_bug!(did, "no generics for {def_id:?}"))?;
208            let wfckresults = genv.check_wf(did)?;
209            AfterSortck::new(genv, &wfckresults)
210                .into_conv_ctxt()
211                .conv_generic_predicates(def_id, generics)
212        }
213        DefKind::OpaqueTy | DefKind::Closure => {
214            Ok(rty::EarlyBinder(rty::GenericPredicates {
215                parent: genv.tcx().predicates_of(def_id).parent,
216                predicates: rty::List::empty(),
217            }))
218        }
219        kind => {
220            Err(query_bug!(
221                def_id.local_id(),
222                "predicates_of called on `{def_id:?}` with kind `{kind:?}`"
223            ))?
224        }
225    }
226}
227
228fn assoc_refinements_of(
229    genv: GlobalEnv,
230    local_id: LocalDefId,
231) -> QueryResult<rty::AssocRefinements> {
232    let local_id = genv.maybe_extern_id(local_id);
233
234    #[allow(
235        clippy::disallowed_methods,
236        reason = "We are iterationg over associated refinemens in fhir, so this is the *source of of truth*"
237    )]
238    let predicates = match &genv.map().expect_item(local_id.local_id())?.kind {
239        fhir::ItemKind::Trait(trait_) => {
240            trait_
241                .assoc_refinements
242                .iter()
243                .map(|assoc_reft| FluxDefId::new(local_id.resolved_id(), assoc_reft.name))
244                .collect()
245        }
246        fhir::ItemKind::Impl(impl_) => {
247            impl_
248                .assoc_refinements
249                .iter()
250                .map(|assoc_reft| FluxDefId::new(local_id.resolved_id(), assoc_reft.name))
251                .collect()
252        }
253        _ => Err(query_bug!(local_id.resolved_id(), "expected trait or impl"))?,
254    };
255    Ok(rty::AssocRefinements { items: predicates })
256}
257
258fn default_assoc_refinement_body(
259    genv: GlobalEnv,
260    trait_assoc_id: FluxId<MaybeExternId>,
261) -> QueryResult<Option<rty::EarlyBinder<rty::Lambda>>> {
262    let trait_id = trait_assoc_id.parent();
263    let assoc_reft = genv
264        .map()
265        .expect_item(trait_id.local_id())?
266        .expect_trait()
267        .find_assoc_reft(trait_assoc_id.name())
268        .unwrap();
269    let Some(body) = assoc_reft.body else { return Ok(None) };
270    let wfckresults = genv.check_wf(trait_id.local_id())?;
271    let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
272    let body = cx.conv_assoc_reft_body(assoc_reft.params, &body, &assoc_reft.output)?;
273    Ok(Some(rty::EarlyBinder(body)))
274}
275
276fn assoc_refinement_body(
277    genv: GlobalEnv,
278    impl_assoc_id: FluxId<MaybeExternId>,
279) -> QueryResult<rty::EarlyBinder<rty::Lambda>> {
280    let impl_id = impl_assoc_id.parent();
281
282    let assoc_reft = genv
283        .map()
284        .expect_item(impl_id.local_id())?
285        .expect_impl()
286        .find_assoc_reft(impl_assoc_id.name())
287        .unwrap();
288
289    let wfckresults = genv.check_wf(impl_id.local_id())?;
290    let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
291    let body = cx.conv_assoc_reft_body(assoc_reft.params, &assoc_reft.body, &assoc_reft.output)?;
292    Ok(rty::EarlyBinder(body))
293}
294
295fn sort_of_assoc_reft(
296    genv: GlobalEnv,
297    assoc_id: FluxId<MaybeExternId>,
298) -> QueryResult<rty::EarlyBinder<rty::FuncSort>> {
299    let container_id = assoc_id.parent();
300
301    match &genv.map().expect_item(container_id.local_id())?.kind {
302        fhir::ItemKind::Trait(trait_) => {
303            let assoc_reft = trait_.find_assoc_reft(assoc_id.name()).unwrap();
304            let wfckresults = WfckResults::new(OwnerId { def_id: container_id.local_id() });
305            let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
306            let inputs = assoc_reft
307                .params
308                .iter()
309                .map(|p| cx.conv_sort(&p.sort))
310                .try_collect_vec()?;
311            let output = cx.conv_sort(&assoc_reft.output)?;
312            Ok(rty::EarlyBinder(rty::FuncSort::new(inputs, output)))
313        }
314        fhir::ItemKind::Impl(impl_) => {
315            let assoc_reft = impl_.find_assoc_reft(assoc_id.name()).unwrap();
316            let wfckresults = WfckResults::new(OwnerId { def_id: container_id.local_id() });
317            let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
318            let inputs = assoc_reft
319                .params
320                .iter()
321                .map(|p| cx.conv_sort(&p.sort))
322                .try_collect_vec()?;
323            let output = cx.conv_sort(&assoc_reft.output)?;
324            Ok(rty::EarlyBinder(rty::FuncSort::new(inputs, output)))
325        }
326        _ => Err(query_bug!(container_id.local_id(), "expected trait or impl")),
327    }
328}
329
330fn item_bounds(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::EarlyBinder<rty::Clauses>> {
331    let def_id = genv.maybe_extern_id(def_id);
332    let parent = genv.tcx().local_parent(def_id.local_id());
333    let wfckresults = genv.check_wf(parent)?;
334    let opaque_ty = genv.map().node(def_id.local_id())?.expect_opaque_ty();
335    Ok(rty::EarlyBinder(
336        AfterSortck::new(genv, &wfckresults)
337            .into_conv_ctxt()
338            .conv_opaque_ty(opaque_ty)?,
339    ))
340}
341
342fn generics_of(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::Generics> {
343    let def_id = genv.maybe_extern_id(def_id);
344    let def_kind = genv.def_kind(def_id);
345    let generics = match def_kind {
346        DefKind::Impl { .. }
347        | DefKind::Struct
348        | DefKind::Enum
349        | DefKind::Union
350        | DefKind::TyAlias
351        | DefKind::AssocFn
352        | DefKind::AssocTy
353        | DefKind::Trait
354        | DefKind::Fn => {
355            let is_trait = def_kind == DefKind::Trait;
356            let generics = genv
357                .map()
358                .get_generics(def_id.local_id())?
359                .ok_or_else(|| query_bug!(def_id.local_id(), "no generics for {def_id:?}"))?;
360            conv::conv_generics(genv, generics, def_id, is_trait)
361        }
362        DefKind::OpaqueTy | DefKind::Closure | DefKind::TraitAlias | DefKind::Ctor(..) => {
363            let rustc_generics = genv.lower_generics_of(def_id);
364            refining::refine_generics(genv, def_id.resolved_id(), &rustc_generics)
365        }
366        kind => {
367            Err(query_bug!(
368                def_id.local_id(),
369                "generics_of called on `{def_id:?}` with kind `{kind:?}`"
370            ))?
371        }
372    };
373    if config::dump_rty() {
374        dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), "generics.rty", &generics).unwrap();
375    }
376    Ok(generics)
377}
378
379fn refinement_generics_of(
380    genv: GlobalEnv,
381    local_id: LocalDefId,
382) -> QueryResult<rty::EarlyBinder<rty::RefinementGenerics>> {
383    let parent = genv.tcx().generics_of(local_id).parent;
384    let parent_count =
385        if let Some(def_id) = parent { genv.refinement_generics_of(def_id)?.count() } else { 0 };
386    let generics = match genv.map().node(local_id)? {
387        fhir::Node::Item(fhir::Item {
388            kind: fhir::ItemKind::Fn(..) | fhir::ItemKind::TyAlias(..),
389            generics,
390            ..
391        })
392        | fhir::Node::TraitItem(fhir::TraitItem {
393            kind: fhir::TraitItemKind::Fn(..),
394            generics,
395            ..
396        })
397        | fhir::Node::ImplItem(fhir::ImplItem {
398            kind: fhir::ImplItemKind::Fn(..), generics, ..
399        }) => {
400            let wfckresults = genv.check_wf(local_id)?;
401            let params = conv::conv_refinement_generics(generics.refinement_params, &wfckresults)?;
402            rty::RefinementGenerics { parent, parent_count, own_params: params }
403        }
404        _ => rty::RefinementGenerics { parent, parent_count, own_params: rty::List::empty() },
405    };
406    Ok(rty::EarlyBinder(generics))
407}
408
409fn type_of(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::EarlyBinder<rty::TyOrCtor>> {
410    let def_id = genv.maybe_extern_id(def_id);
411    let ty = match genv.def_kind(def_id) {
412        DefKind::TyAlias => {
413            let fhir_ty_alias = genv
414                .map()
415                .expect_item(def_id.local_id())?
416                .expect_type_alias();
417            let wfckresults = genv.check_wf(def_id.local_id())?;
418            let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
419            let ty_alias = cx.conv_type_alias(def_id, fhir_ty_alias)?;
420            struct_compat::type_alias(genv, fhir_ty_alias, &ty_alias, def_id)?;
421            rty::TyOrCtor::Ctor(ty_alias)
422        }
423        DefKind::TyParam => {
424            match def_id {
425                MaybeExternId::Local(local_id) => {
426                    let owner = genv.tcx().hir_ty_param_owner(local_id);
427                    let param = genv.map().get_generics(owner)?.unwrap().get_param(local_id);
428                    match param.kind {
429                        fhir::GenericParamKind::Type { default: Some(ty) } => {
430                            let parent = genv.tcx().local_parent(local_id);
431                            let wfckresults = genv.check_wf(parent)?;
432                            conv::conv_default_type_parameter(genv, def_id, &ty, &wfckresults)?
433                                .into()
434                        }
435                        k => Err(query_bug!(local_id, "non-type def def {k:?} {def_id:?}"))?,
436                    }
437                }
438                MaybeExternId::Extern(_, extern_id) => {
439                    let ty = genv.lower_type_of(extern_id)?.skip_binder();
440                    Refiner::default_for_item(genv, ty_param_owner(genv, extern_id))?
441                        .refine_ty_or_base(&ty)?
442                        .into()
443                }
444            }
445        }
446        DefKind::Impl { .. } | DefKind::Struct | DefKind::Enum | DefKind::AssocTy => {
447            let ty = genv.lower_type_of(def_id)?.skip_binder();
448            Refiner::default_for_item(genv, def_id.resolved_id())?
449                .refine_ty_or_base(&ty)?
450                .into()
451        }
452        kind => {
453            Err(query_bug!(
454                def_id.local_id(),
455                "`{:?}` not supported",
456                kind.descr(def_id.resolved_id())
457            ))?
458        }
459    };
460    Ok(rty::EarlyBinder(ty))
461}
462
463fn ty_param_owner(genv: GlobalEnv, def_id: DefId) -> DefId {
464    let def_kind = genv.def_kind(def_id);
465    match def_kind {
466        DefKind::Trait | DefKind::TraitAlias => def_id,
467        DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
468            genv.tcx().parent(def_id)
469        }
470        _ => bug!("ty_param_owner: {:?} is a {:?} not a type parameter", def_id, def_kind),
471    }
472}
473
474fn variants_of(
475    genv: GlobalEnv,
476    def_id: LocalDefId,
477) -> QueryResult<rty::Opaqueness<rty::EarlyBinder<rty::PolyVariants>>> {
478    let def_id = genv.maybe_extern_id(def_id);
479    let local_id = def_id.local_id();
480
481    let item = &genv.map().expect_item(local_id)?;
482    let variants = match &item.kind {
483        fhir::ItemKind::Enum(enum_def) => {
484            let wfckresults = genv.check_wf(local_id)?;
485            let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
486            let variants = cx.conv_enum_variants(def_id, enum_def)?;
487            let variants = rty::List::from_vec(struct_compat::variants(genv, &variants, def_id)?);
488            rty::Opaqueness::Transparent(rty::EarlyBinder(variants))
489        }
490        fhir::ItemKind::Struct(struct_def) => {
491            let wfckresults = genv.check_wf(local_id)?;
492            let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
493            cx.conv_struct_variant(def_id, struct_def)?
494                .map(|variant| -> QueryResult<_> {
495                    let variants = struct_compat::variants(genv, &[variant], def_id)?;
496                    Ok(rty::List::from_vec(variants))
497                })
498                .transpose()?
499                .map(rty::EarlyBinder)
500        }
501        _ => Err(query_bug!(def_id.local_id(), "expected struct or enum"))?,
502    };
503    if config::dump_rty() {
504        dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), "rty", &variants).unwrap();
505    }
506    Ok(variants)
507}
508
509fn fn_sig(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::EarlyBinder<rty::PolyFnSig>> {
510    let def_id = genv.maybe_extern_id(def_id);
511    let fhir_fn_sig = match genv.map().node(def_id.local_id())? {
512        fhir::Node::Item(Item { kind: ItemKind::Fn(fn_sig, ..), .. })
513        | fhir::Node::TraitItem(TraitItem { kind: TraitItemKind::Fn(fn_sig), .. })
514        | fhir::Node::ImplItem(ImplItem { kind: ImplItemKind::Fn(fn_sig), .. })
515        | fhir::Node::ForeignItem(ForeignItem { kind: ForeignItemKind::Fn(fn_sig, ..), .. }) => {
516            Some(fn_sig)
517        }
518        fhir::Node::Ctor => {
519            let tcx = genv.tcx();
520            let variant_id = tcx.parent(def_id.resolved_id());
521            let enum_id = tcx.parent(variant_id);
522            let variant_idx = tcx.adt_def(enum_id).variant_index_with_id(variant_id);
523            let sig = genv
524                .variant_sig(enum_id, variant_idx)?
525                .map(|sig| sig.to_poly_fn_sig(None))
526                .ok_or_else(|| query_bug!("non-transparent enum {enum_id:?} at {variant_idx:?}"))?;
527            return Ok(sig);
528        }
529        _ => None,
530    };
531    let Some(fhir_fn_sig) = fhir_fn_sig else {
532        Err(query_bug!(def_id.local_id(), "expected fn item"))?
533    };
534
535    let wfckresults = genv.check_wf(def_id.local_id())?;
536    let fn_sig = AfterSortck::new(genv, &wfckresults)
537        .into_conv_ctxt()
538        .conv_fn_sig(def_id, fhir_fn_sig)?;
539    let fn_sig = struct_compat::fn_sig(genv, fhir_fn_sig.decl, &fn_sig, def_id)?;
540    let fn_sig = fn_sig.hoist_input_binders();
541
542    if config::dump_rty() {
543        let generics = genv.generics_of(def_id)?;
544        let refinement_generics = genv.refinement_generics_of(def_id)?;
545        dbg::dump_item_info(
546            genv.tcx(),
547            def_id.resolved_id(),
548            "rty",
549            (generics, refinement_generics, &fn_sig),
550        )
551        .unwrap();
552    }
553    Ok(rty::EarlyBinder(fn_sig))
554}
555
556fn check_wf(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<Rc<WfckResults>> {
557    let node = genv.map().expect_owner_node(def_id)?;
558    let wfckresults = wf::check_node(genv, &node)?;
559    Ok(Rc::new(wfckresults))
560}
561
562pub fn check_crate_wf(genv: GlobalEnv) -> Result<(), ErrorGuaranteed> {
563    let errors = Errors::new(genv.sess());
564    for def_id in genv.tcx().hir_crate_items(()).definitions() {
565        if genv.ignored(def_id) || genv.is_dummy(def_id) {
566            continue;
567        }
568        let def_kind = genv.def_kind(def_id);
569        match def_kind {
570            DefKind::TyAlias
571            | DefKind::Struct
572            | DefKind::Enum
573            | DefKind::Fn
574            | DefKind::AssocFn
575            | DefKind::Trait
576            | DefKind::Impl { .. }
577            // we skip checking the DefKind::OpaqueTy because they
578            // must be wf-checked (and desugared) in the context of
579            // their "parent", so we do so "lazily" when the appropriate
580            // query is called on the "parent"
581            => {
582                let _ = genv.check_wf(def_id).emit(&errors);
583            }
584            _ => {}
585        }
586    }
587
588    // Query qualifiers and spec funcs to report wf errors
589    let _ = genv.qualifiers().emit(&errors);
590    let _ = genv.normalized_defns(LOCAL_CRATE);
591
592    errors.into_result()
593}
594
595mod errors {
596    use flux_errors::E0999;
597    use flux_macros::Diagnostic;
598    use flux_middle::def_id::FluxLocalDefId;
599    use rustc_span::Span;
600
601    #[derive(Diagnostic)]
602    #[diag(fhir_analysis_definition_cycle, code = E0999)]
603    pub struct DefinitionCycle {
604        #[primary_span]
605        #[label]
606        span: Span,
607        msg: String,
608    }
609
610    impl DefinitionCycle {
611        pub(super) fn new(span: Span, cycle: Vec<FluxLocalDefId>) -> Self {
612            let root = format!("`{}`", cycle[0].name());
613            let names: Vec<String> = cycle.iter().map(|s| format!("`{}`", s.name())).collect();
614            let msg = format!("{} -> {}", names.join(" -> "), root);
615            Self { span, msg }
616        }
617    }
618}