flux_fhir_analysis/
lib.rs

1#![feature(rustc_private)]
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;
17use std::{iter, rc::Rc};
18
19use conv::{AfterSortck, ConvPhase, struct_compat};
20use flux_common::{
21    bug, dbg,
22    iter::IterExt,
23    result::{ErrorEmitter as _, ResultExt},
24};
25use flux_config as config;
26use flux_errors::Errors;
27use flux_middle::{
28    def_id::{FluxDefId, FluxId, MaybeExternId},
29    fhir::{
30        self, ForeignItem, ForeignItemKind, ImplItem, ImplItemKind, Item, ItemKind, TraitItem,
31        TraitItemKind, visit::Visitor as _,
32    },
33    global_env::GlobalEnv,
34    queries::{Providers, QueryErr, QueryResult},
35    query_bug,
36    rty::{
37        self, AssocReft, Binder, WfckResults,
38        fold::TypeFoldable,
39        refining::{self, Refiner},
40    },
41};
42use flux_rustc_bridge::lowering::Lower;
43use itertools::Itertools;
44use rustc_abi::FIRST_VARIANT;
45use rustc_data_structures::unord::{UnordMap, UnordSet};
46use rustc_errors::ErrorGuaranteed;
47use rustc_hir::{
48    OwnerId,
49    def::{CtorOf, DefKind},
50    def_id::{DefId, LocalDefId},
51};
52use rustc_span::Span;
53
54pub fn provide(providers: &mut Providers) {
55    providers.spec_funcs = spec_funcs;
56    providers.func_sort = func_sort;
57    providers.func_span = flux_def_ident_span;
58    providers.qualifiers = qualifiers;
59    providers.axioms = axioms;
60    providers.prim_rel = prim_rel;
61    providers.adt_sort_def_of = adt_sort_def_of;
62    providers.check_wf = check_wf;
63    providers.late_bound_refinement_params = late_bound_refinement_params;
64    providers.adt_def = adt_def;
65    providers.invariants_of = invariants_of;
66    providers.constant_info = constant_info;
67    providers.static_info = static_info;
68    providers.type_of = type_of;
69    providers.variants_of = variants_of;
70    providers.fn_sig = fn_sig;
71    providers.generics_of = generics_of;
72    providers.refinement_generics_of = refinement_generics_of;
73    providers.predicates_of = predicates_of;
74    providers.assoc_refinements_of = assoc_refinements_of;
75    providers.sort_of_assoc_reft = sort_of_assoc_reft;
76    providers.assoc_refinement_body = assoc_refinement_body;
77    providers.default_assoc_refinement_body = default_assoc_refinement_body;
78    providers.item_bounds = item_bounds;
79    providers.sort_decl_param_count = sort_decl_param_count;
80}
81
82fn sort_decl_param_count(genv: GlobalEnv, def_id: FluxId<MaybeExternId>) -> usize {
83    genv.fhir_sort_decl(def_id.local_id()).unwrap().params
84}
85
86fn adt_sort_def_of(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::AdtSortDef> {
87    let kind = genv.fhir_expect_refinement_kind(def_id.local_id())?;
88    conv::conv_adt_sort_def(genv, def_id, kind)
89}
90
91fn func_sort(genv: GlobalEnv, def_id: FluxId<MaybeExternId>) -> rty::PolyFuncSort {
92    let func = genv.fhir_spec_func_body(def_id.local_id()).unwrap();
93    match conv::conv_func_decl(genv, func).emit(&genv) {
94        Ok(normalized) => normalized,
95        Err(err) => {
96            genv.sess().abort(err);
97        }
98    }
99}
100
101fn flux_def_ident_span(genv: GlobalEnv, def_id: FluxId<MaybeExternId>) -> Span {
102    genv.fhir_spec_func_body(def_id.local_id())
103        .unwrap()
104        .ident_span
105}
106
107fn spec_funcs(genv: GlobalEnv) -> rty::SpecFuncs {
108    match try_spec_funcs(genv) {
109        Ok(funcs) => funcs,
110        Err(err) => {
111            genv.sess().abort(err);
112        }
113    }
114}
115
116fn try_spec_funcs(genv: GlobalEnv) -> Result<rty::SpecFuncs, ErrorGuaranteed> {
117    let mut funcs = vec![];
118
119    // Collect and emit all errors
120    let mut errors = Errors::new(genv.sess());
121    for (_, item) in genv.fhir_iter_flux_items() {
122        let fhir::FluxItem::Func(func) = item else { continue };
123        let Some(wfckresults) = wf::check_flux_item(genv, item).collect_err(&mut errors) else {
124            continue;
125        };
126        let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
127        let Ok(spec_func) = cx.conv_spec_func(func).emit(&errors) else { continue };
128        funcs.push((func.def_id, spec_func));
129    }
130    errors.to_result()?;
131
132    rty::SpecFuncs::new(funcs)
133        .map_err(|cycle| {
134            let span = genv
135                .fhir_spec_func_body(cycle[0])
136                .unwrap()
137                .body
138                .unwrap()
139                .span;
140            errors::DefinitionCycle::new(span, cycle)
141        })
142        .emit(&genv)
143}
144
145fn qualifiers(genv: GlobalEnv) -> QueryResult<Vec<rty::Qualifier>> {
146    genv.fhir_qualifiers()
147        .map(|qualifier| {
148            let wfckresults = wf::check_flux_item(genv, fhir::FluxItem::Qualifier(qualifier))?;
149            Ok(AfterSortck::new(genv, &wfckresults)
150                .into_conv_ctxt()
151                .conv_qualifier(qualifier)?
152                .reduce(genv))
153        })
154        .try_collect()
155}
156
157fn axioms(genv: GlobalEnv) -> QueryResult<Vec<rty::Axiom>> {
158    genv.fhir_axioms()
159        .map(|axiom| {
160            let wfckresults = wf::check_flux_item(genv, fhir::FluxItem::Axiom(axiom))?;
161            let body = AfterSortck::new(genv, &wfckresults)
162                .into_conv_ctxt()
163                .conv_axiom(axiom)?
164                .reduce(genv);
165            // The patterns are computed here, *after* reducing the body, so it is only done
166            // once (instead of once per query).
167            rty::Axiom::new(genv, axiom.def_id, body).map_err(|rty::UncoveredAxiomVar(var)| {
168                let param = &axiom.args[var.as_usize()];
169                QueryErr::Emitted(
170                    genv.emit(errors::IllFormedAxiom::new(axiom.span, param.span, param.name)),
171                )
172            })
173        })
174        .try_collect()
175}
176
177fn primop_props(genv: GlobalEnv) -> QueryResult<Vec<rty::PrimOpProp>> {
178    genv.fhir_primop_props()
179        .map(|primop_prop| {
180            let wfckresults = wf::check_flux_item(genv, fhir::FluxItem::PrimOpProp(primop_prop))?;
181            Ok(AfterSortck::new(genv, &wfckresults)
182                .into_conv_ctxt()
183                .conv_primop_prop(primop_prop)?
184                .reduce(genv))
185        })
186        .try_collect()
187}
188
189fn conjoin_bind_exprs(exprs: Vec<Binder<rty::Expr>>) -> Binder<rty::Expr> {
190    let mut iter = exprs.into_iter();
191    let first = iter.next().unwrap();
192    let sorts = first.sorts();
193    let bodies = iter::once(first.skip_binder()).chain(iter.map(|expr| expr.skip_binder()));
194    let expr = rty::Expr::and_from_iter(bodies);
195    Binder::bind_with_sorts(expr, &sorts)
196}
197
198fn prim_rel(genv: GlobalEnv) -> QueryResult<UnordMap<rty::BinOp, rty::PrimRel>> {
199    let primop_props = primop_props(genv)?
200        .into_iter()
201        .into_group_map_by(|primop_prop| primop_prop.op.clone());
202
203    let mut res = UnordMap::default();
204    for (op, props) in primop_props {
205        let exprs = props
206            .iter()
207            .map(|prop| prop.body.clone())
208            .collect::<Vec<_>>();
209        let body = conjoin_bind_exprs(exprs);
210        res.insert(op, rty::PrimRel { body });
211    }
212    Ok(res)
213}
214
215fn adt_def(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::AdtDef> {
216    let item = genv.fhir_expect_item(def_id.local_id())?;
217
218    let adt_def = genv.tcx().adt_def(def_id.resolved_id()).lower(genv.tcx());
219
220    let is_opaque = matches!(item.kind, fhir::ItemKind::Struct(def) if def.is_opaque());
221
222    Ok(rty::AdtDef::new(adt_def, genv.adt_sort_def_of(def_id)?, is_opaque))
223}
224
225fn constant_info(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::ConstantInfo> {
226    let node = genv.fhir_node(def_id.local_id())?;
227    let Some(sort) = genv.sort_of_def_id(def_id.resolved_id()).emit(&genv)? else {
228        return Ok(rty::ConstantInfo::Uninterpreted);
229    };
230    let tcx = genv.tcx();
231    match node {
232        fhir::Node::Item(fhir::Item { kind: fhir::ItemKind::Const(Some(expr)), .. }) => {
233            // If the constant has a `#[consant(expr)]` annotation we use that
234            let owner = def_id.map(|def_id| rustc_hir::OwnerId { def_id });
235            let wfckresults = wf::check_constant_expr(genv, owner, expr, &sort)?;
236            let expr = AfterSortck::new(genv, &wfckresults)
237                .into_conv_ctxt()
238                .conv_constant_expr(expr)?;
239            Ok(rty::ConstantInfo::Interpreted(expr, sort))
240        }
241        fhir::Node::Item(fhir::Item { kind: fhir::ItemKind::Const(None), .. })
242        | fhir::Node::AnonConst
243        | fhir::Node::ImplItem(fhir::ImplItem { kind: fhir::ImplItemKind::Const, .. }) => {
244            // For other constants, we try to evaluate them if they are integral
245            if let Some(ty) = tcx.type_of(def_id).no_bound_vars()
246                && ty.is_integral()
247                && let Ok(val) = tcx.const_eval_poly(def_id.resolved_id())
248                && let Some(val) = val.try_to_scalar_int()
249                && let Some(constant_) = rty::Constant::from_scalar_int(tcx, val, &ty)
250            {
251                // FIXME(nilehmann) we should probably report an error in case const evaluation
252                // fails instead of silently ignore it.
253                Ok(rty::ConstantInfo::Interpreted(rty::Expr::constant(constant_), rty::Sort::Int))
254            } else {
255                Ok(rty::ConstantInfo::Uninterpreted)
256            }
257        }
258        fhir::Node::TraitItem(fhir::TraitItem { kind: fhir::TraitItemKind::Const, .. }) => {
259            Ok(rty::ConstantInfo::Uninterpreted)
260        }
261        _ => Err(query_bug!(def_id.local_id(), "expected const item"))?,
262    }
263}
264
265/// The type of a static: its spec if it has one, or the default refinement of its rust type.
266fn static_info(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::Ty> {
267    if let fhir::Node::Item(fhir::Item { kind: fhir::ItemKind::Static(Some(ty)), .. }) =
268        genv.fhir_node(def_id.local_id())?
269    {
270        let wfckresults = genv.check_wf(def_id.local_id())?;
271        AfterSortck::new(genv, &wfckresults)
272            .into_conv_ctxt()
273            .conv_static_ty(ty)
274    } else {
275        rty::refining::default_static_ty(genv, def_id.resolved_id())
276    }
277}
278
279/// Errors are reported at the definition of the adt. If the invariants fail to convert, we
280/// continue as if the adt had no invariants. This is sound because the invariants are then
281/// neither checked (when constructing the adt) nor assumed (when using it).
282fn invariants_of(
283    genv: GlobalEnv,
284    def_id: MaybeExternId,
285) -> rty::EarlyBinder<rty::List<rty::Invariant>> {
286    let invariants = try_invariants_of(genv, def_id).unwrap_or_else(|err| {
287        if !matches!(err, QueryErr::Emitted(_)) {
288            genv.emit(err);
289        }
290        vec![]
291    });
292    rty::EarlyBinder(rty::List::from_vec(invariants))
293}
294
295fn try_invariants_of(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<Vec<rty::Invariant>> {
296    let item = genv.fhir_expect_item(def_id.local_id())?;
297    let (params, invariants) = match &item.kind {
298        fhir::ItemKind::Enum(enum_def) => (enum_def.params, enum_def.invariants),
299        fhir::ItemKind::Struct(struct_def) => (struct_def.params, struct_def.invariants),
300        _ => Err(query_bug!(item.owner_id.local_id(), "expected struct or enum"))?,
301    };
302    let wfckresults = wf::check_invariants(genv, item.owner_id, params, invariants)?;
303    AfterSortck::new(genv, &wfckresults)
304        .into_conv_ctxt()
305        .conv_invariants(item.owner_id.map(|it| it.def_id), params, invariants)
306}
307
308fn predicates_of(
309    genv: GlobalEnv,
310    def_id: MaybeExternId,
311) -> QueryResult<rty::EarlyBinder<rty::GenericPredicates>> {
312    match genv.def_kind(def_id) {
313        DefKind::Impl { .. }
314        | DefKind::Struct
315        | DefKind::Enum
316        | DefKind::Union
317        | DefKind::TyAlias
318        | DefKind::AssocFn
319        | DefKind::AssocTy
320        | DefKind::Trait
321        | DefKind::Fn => {
322            let did = def_id.local_id();
323            let generics = genv
324                .fhir_get_generics(did)?
325                .ok_or_else(|| query_bug!(did, "no generics for {def_id:?}"))?;
326            let wfckresults = genv.check_wf(did)?;
327            AfterSortck::new(genv, &wfckresults)
328                .into_conv_ctxt()
329                .conv_generic_predicates(def_id, generics)
330        }
331        DefKind::OpaqueTy | DefKind::Closure | DefKind::Static { .. } => {
332            Ok(rty::EarlyBinder(rty::GenericPredicates {
333                parent: genv.tcx().clauses_of(def_id).parent,
334                predicates: rty::List::empty(),
335            }))
336        }
337        kind => {
338            Err(query_bug!(
339                def_id.local_id(),
340                "predicates_of called on `{def_id:?}` with kind `{kind:?}`"
341            ))?
342        }
343    }
344}
345
346fn assoc_refinements_of(
347    genv: GlobalEnv,
348    def_id: MaybeExternId,
349) -> QueryResult<rty::AssocRefinements> {
350    #[allow(
351        clippy::disallowed_methods,
352        reason = "We are iterationg over associated refinemens in fhir, so this is the *source of of truth*"
353    )]
354    let predicates = match &genv.fhir_expect_item(def_id.local_id())?.kind {
355        fhir::ItemKind::Trait(trait_) => {
356            trait_
357                .assoc_refinements
358                .iter()
359                .map(|assoc_reft| {
360                    AssocReft::new(
361                        FluxDefId::new(def_id.resolved_id(), assoc_reft.name),
362                        assoc_reft.final_,
363                        assoc_reft.span,
364                    )
365                })
366                .collect()
367        }
368        fhir::ItemKind::Impl(impl_) => {
369            impl_
370                .assoc_refinements
371                .iter()
372                .map(|assoc_reft| {
373                    AssocReft::new(
374                        FluxDefId::new(def_id.resolved_id(), assoc_reft.name),
375                        false,
376                        assoc_reft.span,
377                    )
378                })
379                .collect()
380        }
381        _ => Err(query_bug!(def_id.resolved_id(), "expected trait or impl"))?,
382    };
383    Ok(rty::AssocRefinements { items: predicates })
384}
385
386fn default_assoc_refinement_body(
387    genv: GlobalEnv,
388    trait_assoc_id: FluxId<MaybeExternId>,
389) -> QueryResult<Option<rty::EarlyBinder<rty::Lambda>>> {
390    let trait_id = trait_assoc_id.parent();
391    let assoc_reft = genv
392        .fhir_expect_item(trait_id.local_id())?
393        .expect_trait()
394        .find_assoc_reft(trait_assoc_id.name())
395        .unwrap();
396    let Some(body) = assoc_reft.body else { return Ok(None) };
397    let wfckresults = genv.check_wf(trait_id.local_id())?;
398    let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
399    let body = cx.conv_assoc_reft_body(assoc_reft.params, &body, &assoc_reft.output)?;
400    Ok(Some(rty::EarlyBinder(body)))
401}
402
403fn assoc_refinement_body(
404    genv: GlobalEnv,
405    impl_assoc_id: FluxId<MaybeExternId>,
406) -> QueryResult<rty::EarlyBinder<rty::Lambda>> {
407    let impl_id = impl_assoc_id.parent();
408
409    let assoc_reft = genv
410        .fhir_expect_item(impl_id.local_id())?
411        .expect_impl()
412        .find_assoc_reft(impl_assoc_id.name())
413        .unwrap();
414
415    let wfckresults = genv.check_wf(impl_id.local_id())?;
416    let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
417    let body = cx.conv_assoc_reft_body(assoc_reft.params, &assoc_reft.body, &assoc_reft.output)?;
418    Ok(rty::EarlyBinder(body))
419}
420
421fn sort_of_assoc_reft(
422    genv: GlobalEnv,
423    assoc_id: FluxId<MaybeExternId>,
424) -> QueryResult<rty::EarlyBinder<rty::FuncSort>> {
425    let container_id = assoc_id.parent();
426
427    match &genv.fhir_expect_item(container_id.local_id())?.kind {
428        fhir::ItemKind::Trait(trait_) => {
429            let assoc_reft = trait_.find_assoc_reft(assoc_id.name()).unwrap();
430            let wfckresults = WfckResults::new(container_id.map(|def_id| OwnerId { def_id }));
431            let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
432            let inputs = assoc_reft
433                .params
434                .iter()
435                .map(|p| cx.conv_sort(&p.sort))
436                .try_collect_vec()?;
437            let output = cx.conv_sort(&assoc_reft.output)?;
438            Ok(rty::EarlyBinder(rty::FuncSort::new(inputs, output)))
439        }
440        fhir::ItemKind::Impl(impl_) => {
441            let assoc_reft = impl_.find_assoc_reft(assoc_id.name()).unwrap();
442            let wfckresults = WfckResults::new(container_id.map(|def_id| OwnerId { def_id }));
443            let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
444            let inputs = assoc_reft
445                .params
446                .iter()
447                .map(|p| cx.conv_sort(&p.sort))
448                .try_collect_vec()?;
449            let output = cx.conv_sort(&assoc_reft.output)?;
450            Ok(rty::EarlyBinder(rty::FuncSort::new(inputs, output)))
451        }
452        _ => Err(query_bug!(container_id.local_id(), "expected trait or impl")),
453    }
454}
455
456fn item_bounds(
457    genv: GlobalEnv,
458    def_id: MaybeExternId,
459) -> QueryResult<rty::EarlyBinder<rty::Clauses>> {
460    let parent = genv.tcx().local_parent(def_id.local_id());
461    let wfckresults = genv.check_wf(parent)?;
462    let opaque_ty = genv.fhir_node(def_id.local_id())?.expect_opaque_ty();
463    Ok(rty::EarlyBinder(
464        AfterSortck::new(genv, &wfckresults)
465            .into_conv_ctxt()
466            .conv_opaque_ty(opaque_ty)?,
467    ))
468}
469
470fn generics_of(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::Generics> {
471    let def_kind = genv.def_kind(def_id);
472    let generics = match def_kind {
473        DefKind::Impl { .. }
474        | DefKind::Struct
475        | DefKind::Enum
476        | DefKind::Union
477        | DefKind::TyAlias
478        | DefKind::AssocFn
479        | DefKind::AssocTy
480        | DefKind::Trait
481        | DefKind::Fn => {
482            let is_trait = def_kind == DefKind::Trait;
483            let generics = genv
484                .fhir_get_generics(def_id.local_id())?
485                .ok_or_else(|| query_bug!(def_id.local_id(), "no generics for {def_id:?}"))?;
486            conv::conv_generics(genv, generics, def_id, is_trait)
487        }
488        DefKind::OpaqueTy
489        | DefKind::Closure
490        | DefKind::TraitAlias
491        | DefKind::Ctor(..)
492        | DefKind::Static { .. } => refining::refine_generics(&genv.lower_generics_of(def_id)),
493        kind => {
494            Err(query_bug!(
495                def_id.local_id(),
496                "generics_of called on `{def_id:?}` with kind `{kind:?}`"
497            ))?
498        }
499    };
500    if config::dump_rty() {
501        dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), "generics.rty", &generics).unwrap();
502    }
503    Ok(generics)
504}
505
506/// See [`GlobalEnv::late_bound_refinement_params`]
507fn late_bound_refinement_params<'genv>(
508    genv: GlobalEnv<'genv, '_>,
509    def_id: LocalDefId,
510) -> QueryResult<&'genv [fhir::ParamId]> {
511    let node = genv.fhir_expect_owner_node(def_id)?;
512    let Some(fn_sig) = node.fn_sig() else { return Ok(&[]) };
513    let generics = node.generics();
514
515    // Where-clauses and opaque types are converted separately from the signature (as clauses of the
516    // item or the opaque type), so params mentioned there must be early bound.
517    let mut appears_in_clauses = ParamCollector::default();
518    for pred in generics.predicates.unwrap_or_default() {
519        appears_in_clauses.visit_where_predicate(pred);
520    }
521    OpaqueTyParamCollector(&mut appears_in_clauses).visit_fn_sig(fn_sig);
522
523    let late_bound = generics
524        .refinement_params
525        .iter()
526        // Locations are always early bound
527        .filter(|param| !param.kind.is_loc() && !matches!(param.sort, fhir::Sort::Loc))
528        .filter(|param| !appears_in_clauses.params.contains(&param.id))
529        .map(|param| param.id)
530        .collect_vec();
531    Ok(genv.alloc_slice(&late_bound))
532}
533
534/// Collects all refinement params mentioned in the visited nodes.
535#[derive(Default)]
536struct ParamCollector {
537    params: UnordSet<fhir::ParamId>,
538}
539
540impl<'fhir> fhir::visit::Visitor<'fhir> for ParamCollector {
541    fn visit_path_expr(&mut self, path: &fhir::PathExpr<'fhir>) {
542        if let fhir::Res::Param(_, id) = path.res {
543            self.params.insert(id);
544        }
545    }
546}
547
548/// Collects the refinement params mentioned in the bounds of opaque types.
549struct OpaqueTyParamCollector<'a>(&'a mut ParamCollector);
550
551impl<'fhir> fhir::visit::Visitor<'fhir> for OpaqueTyParamCollector<'_> {
552    fn visit_opaque_ty(&mut self, opaque_ty: &fhir::OpaqueTy<'fhir>) {
553        self.0.visit_opaque_ty(opaque_ty);
554    }
555}
556
557fn refinement_generics_of(
558    genv: GlobalEnv,
559    def_id: MaybeExternId,
560) -> QueryResult<rty::EarlyBinder<rty::RefinementGenerics>> {
561    let parent = genv.tcx().generics_of(def_id).parent;
562    let parent_count =
563        if let Some(def_id) = parent { genv.refinement_generics_of(def_id)?.count() } else { 0 };
564    let generics = match genv.fhir_node(def_id.local_id())? {
565        fhir::Node::Item(fhir::Item {
566            kind: fhir::ItemKind::Fn(..) | fhir::ItemKind::TyAlias(..),
567            ..
568        })
569        | fhir::Node::TraitItem(fhir::TraitItem { kind: fhir::TraitItemKind::Fn(..), .. })
570        | fhir::Node::ImplItem(fhir::ImplItem { kind: fhir::ImplItemKind::Fn(..), .. })
571        | fhir::Node::ForeignItem(fhir::ForeignItem {
572            kind: fhir::ForeignItemKind::Fn(..), ..
573        }) => {
574            let wfckresults = genv.check_wf(def_id.local_id())?;
575            let (early, _) = genv.fhir_split_refinement_params(def_id.local_id())?;
576            let params = conv::conv_refinement_generics(&early, &wfckresults)?;
577            rty::RefinementGenerics { parent, parent_count, own_params: params }
578        }
579        _ => rty::RefinementGenerics { parent, parent_count, own_params: rty::List::empty() },
580    };
581    Ok(rty::EarlyBinder(generics))
582}
583
584fn type_of(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::EarlyBinder<rty::TyOrCtor>> {
585    let ty = match genv.def_kind(def_id) {
586        DefKind::TyAlias => {
587            let fhir_ty_alias = genv
588                .fhir_expect_item(def_id.local_id())?
589                .expect_type_alias();
590            let wfckresults = genv.check_wf(def_id.local_id())?;
591            let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
592            let ty_alias = cx.conv_type_alias(def_id, fhir_ty_alias)?;
593            struct_compat::type_alias(genv, fhir_ty_alias, &ty_alias, def_id)?;
594            rty::TyOrCtor::Ctor(ty_alias)
595        }
596        DefKind::TyParam => {
597            match def_id {
598                MaybeExternId::Local(local_id) => {
599                    let owner = genv.tcx().hir_ty_param_owner(local_id);
600                    let param = genv.fhir_get_generics(owner)?.unwrap().get_param(local_id);
601                    match param.kind {
602                        fhir::GenericParamKind::Type { default: Some(ty) } => {
603                            let parent = genv.tcx().local_parent(local_id);
604                            let wfckresults = genv.check_wf(parent)?;
605                            conv::conv_default_type_parameter(genv, def_id, &ty, &wfckresults)?
606                                .into()
607                        }
608                        k => Err(query_bug!(local_id, "non-type def def {k:?} {def_id:?}"))?,
609                    }
610                }
611                MaybeExternId::Extern(_, extern_id) => {
612                    let ty = genv.lower_type_of(extern_id)?.skip_binder();
613                    Refiner::default_for_item(genv, ty_param_owner(genv, extern_id))?
614                        .refine_ty_or_base(&ty)?
615                        .into()
616                }
617            }
618        }
619        DefKind::Impl { .. } | DefKind::Struct | DefKind::Enum | DefKind::AssocTy => {
620            let ty = genv.lower_type_of(def_id)?.skip_binder();
621            Refiner::default_for_item(genv, def_id.resolved_id())?
622                .refine_ty_or_base(&ty)?
623                .into()
624        }
625        kind => {
626            Err(query_bug!(
627                def_id.local_id(),
628                "`{:?}` not supported",
629                kind.descr(def_id.resolved_id())
630            ))?
631        }
632    };
633    Ok(rty::EarlyBinder(ty))
634}
635
636fn ty_param_owner(genv: GlobalEnv, def_id: DefId) -> DefId {
637    let def_kind = genv.def_kind(def_id);
638    match def_kind {
639        DefKind::Trait | DefKind::TraitAlias => def_id,
640        DefKind::LifetimeParam | DefKind::TyParam | DefKind::ConstParam => {
641            genv.tcx().parent(def_id)
642        }
643        _ => bug!("ty_param_owner: {:?} is a {:?} not a type parameter", def_id, def_kind),
644    }
645}
646
647fn variants_of(
648    genv: GlobalEnv,
649    def_id: MaybeExternId,
650) -> QueryResult<rty::Opaqueness<rty::EarlyBinder<rty::PolyVariants>>> {
651    let local_id = def_id.local_id();
652
653    let item = &genv.fhir_expect_item(local_id)?;
654    let variants = match &item.kind {
655        fhir::ItemKind::Enum(enum_def) => {
656            let wfckresults = genv.check_wf(local_id)?;
657            let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
658            let variants = cx.conv_enum_variants(def_id, enum_def)?;
659            let variants = rty::List::from_vec(struct_compat::variants(genv, &variants, def_id)?);
660            rty::Opaqueness::Transparent(rty::EarlyBinder(variants))
661        }
662        fhir::ItemKind::Struct(struct_def) => {
663            let wfckresults = genv.check_wf(local_id)?;
664            let mut cx = AfterSortck::new(genv, &wfckresults).into_conv_ctxt();
665            cx.conv_struct_variant(def_id, struct_def)?
666                .map(|variant| -> QueryResult<_> {
667                    let variants = struct_compat::variants(genv, &[variant], def_id)?;
668                    Ok(rty::List::from_vec(variants))
669                })
670                .transpose()?
671                .map(rty::EarlyBinder)
672        }
673        _ => Err(query_bug!(def_id.local_id(), "expected struct or enum"))?,
674    };
675    if config::dump_rty() {
676        dbg::dump_item_info(genv.tcx(), def_id.resolved_id(), "rty", &variants).unwrap();
677    }
678    Ok(variants)
679}
680
681fn fn_sig(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult<rty::EarlyBinder<rty::PolyFnSig>> {
682    let fhir_node = genv.fhir_node(def_id.local_id())?;
683    match &fhir_node {
684        fhir::Node::Item(Item { kind: ItemKind::Fn(fhir_fn_sig, ..), .. })
685        | fhir::Node::TraitItem(TraitItem { kind: TraitItemKind::Fn(fhir_fn_sig), .. })
686        | fhir::Node::ImplItem(ImplItem { kind: ImplItemKind::Fn(fhir_fn_sig), .. })
687        | fhir::Node::ForeignItem(ForeignItem {
688            kind: ForeignItemKind::Fn(fhir_fn_sig, ..), ..
689        }) => {
690            let wfckresults = genv.check_wf(def_id.local_id())?;
691            let fn_sig = AfterSortck::new(genv, &wfckresults)
692                .into_conv_ctxt()
693                .conv_fn_sig(def_id, fhir_fn_sig)?;
694            let fn_sig = struct_compat::fn_sig(genv, fhir_fn_sig.decl, &fn_sig, def_id)?;
695            let mut fn_sig =
696                if config::suggestions() { fn_sig.hoist_input_binders() } else { fn_sig };
697            // We aren't sure how to handle suggestions for Traits themselves
698            // and ForeignItems.
699            //
700            // Things get a bit messy with making ImplItem suggestions match the
701            // subtype for their parent trait, but for now we *will* offer them
702            // as suggestions; the user can resolve issues.
703            if !genv.no_suggestions(def_id.local_id())
704                && !matches!(fhir_node, fhir::Node::TraitItem(..) | fhir::Node::ForeignItem(..))
705            {
706                fn_sig = fn_sig.add_weak_kvars(genv, def_id.resolved_id())?;
707            }
708
709            if config::dump_rty() {
710                let generics = genv.generics_of(def_id)?;
711                let refinement_generics = genv.refinement_generics_of(def_id)?;
712                dbg::dump_item_info(
713                    genv.tcx(),
714                    def_id.resolved_id(),
715                    "rty",
716                    (generics, refinement_generics, &fn_sig),
717                )
718                .unwrap();
719            }
720            Ok(rty::EarlyBinder(fn_sig))
721        }
722        fhir::Node::Ctor => {
723            let tcx = genv.tcx();
724            let (adt_id, variant_idx) = match tcx.def_kind(def_id) {
725                DefKind::Ctor(CtorOf::Struct, _) => {
726                    let struct_id = tcx.parent(def_id.resolved_id());
727                    (struct_id, FIRST_VARIANT)
728                }
729                DefKind::Ctor(CtorOf::Variant, _) => {
730                    let variant_id = tcx.parent(def_id.resolved_id());
731                    let enum_id = tcx.parent(variant_id);
732                    let variant_idx = tcx.adt_def(enum_id).variant_index_with_id(variant_id);
733                    (enum_id, variant_idx)
734                }
735                _ => return Err(query_bug!("invalid `DefKind` for ctor node")),
736            };
737            genv.variant_sig(adt_id, variant_idx)?
738                .map(|sig| sig.to_poly_fn_sig(None))
739                .ok_or_query_err(adt_id)
740        }
741        node => Err(query_bug!("fn_sig called on unsupported node {node:?}")),
742    }
743}
744
745fn check_wf(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<Rc<WfckResults>> {
746    let node = genv.fhir_expect_owner_node(def_id)?;
747    let wfckresults = wf::check_node(genv, &node)?;
748    Ok(Rc::new(wfckresults))
749}
750
751mod errors {
752    use flux_errors::E0999;
753    use flux_macros::Diagnostic;
754    use flux_middle::def_id::FluxLocalDefId;
755    use rustc_span::{Span, Symbol};
756
757    #[derive(Diagnostic)]
758    #[diag("cycle in definitions", code = E0999)]
759    pub struct DefinitionCycle {
760        #[primary_span]
761        #[label("{$msg}")]
762        span: Span,
763        msg: String,
764    }
765
766    #[derive(Diagnostic)]
767    #[diag("ill-formed axiom", code = E0999)]
768    #[note(
769        "every variable of an axiom must occur in an application of an uninterpreted function, which is used to instantiate the axiom"
770    )]
771    pub struct IllFormedAxiom {
772        #[primary_span]
773        span: Span,
774        #[label("`{$name}` does not occur in any application (trigger pattern) of the axiom")]
775        param_span: Span,
776        name: Symbol,
777    }
778
779    impl IllFormedAxiom {
780        pub(super) fn new(span: Span, param_span: Span, name: Symbol) -> Self {
781            Self { span, param_span, name }
782        }
783    }
784
785    impl DefinitionCycle {
786        pub(super) fn new(span: Span, cycle: Vec<FluxLocalDefId>) -> Self {
787            let root = format!("`{}`", cycle[0].name());
788            let names: Vec<String> = cycle.iter().map(|s| format!("`{}`", s.name())).collect();
789            let msg = format!("{} -> {}", names.join(" -> "), root);
790            Self { span, msg }
791        }
792    }
793}
flux_fhir_analysis/lib.rs

flux_fhir_analysis/
lib.rs
