flux_fhir_analysis/wf/
mod.rs

1//! Checks type well-formedness
2//!
3//! Well-formedness checking assumes names are correctly bound which is guaranteed after desugaring.
4
5mod errors;
6mod param_usage;
7mod sortck;
8
9use flux_common::result::{ErrorCollector, ResultExt as _};
10use flux_errors::Errors;
11use flux_middle::{
12    def_id::MaybeExternId,
13    fhir::{self, FhirId, FluxOwnerId, visit::Visitor},
14    global_env::GlobalEnv,
15    queries::QueryResult,
16    rty::{self, RecordCtor, WfckResults},
17};
18use rustc_data_structures::unord::UnordSet;
19use rustc_errors::ErrorGuaranteed;
20use rustc_hir::{
21    OwnerId,
22    def::DefKind,
23    def_id::{CrateNum, DefId, DefIndex, LocalDefId},
24};
25
26use self::sortck::{ImplicitParamInferer, InferCtxt};
27use crate::{
28    conv::{ConvPhase, WfckResultsProvider},
29    wf::sortck::prim_op_sort,
30};
31
32type Result<T = ()> = std::result::Result<T, ErrorGuaranteed>;
33
34pub(crate) fn check_flux_item<'genv>(
35    genv: GlobalEnv<'genv, '_>,
36    item: fhir::FluxItem<'genv>,
37) -> Result<WfckResults> {
38    let owner = FluxOwnerId::Flux(item.def_id());
39    let mut infcx = InferCtxt::new(genv, owner);
40
41    Wf::with(&mut infcx, |wf| {
42        wf.init_infcx_for_flux_item(item).emit(&genv)?;
43        wf.check_flux_item(item);
44        Ok(())
45    })?;
46    infcx.into_results()
47}
48
49pub(crate) fn check_constant_expr<'genv>(
50    genv: GlobalEnv<'genv, '_>,
51    owner: MaybeExternId<OwnerId>,
52    expr: &fhir::Expr<'genv>,
53    sort: &rty::Sort,
54) -> Result<WfckResults> {
55    let mut infcx = InferCtxt::new(genv, FluxOwnerId::Rust(owner));
56    Wf::with(&mut infcx, |wf| {
57        wf.declare_params_in_expr(expr)?;
58        wf.as_conv_ctxt()
59            .conv_constant_expr(expr)
60            .emit(&wf.errors)?;
61        wf.check_expr(expr, sort);
62        Ok(())
63    })?;
64    infcx.into_results()
65}
66
67pub(crate) fn check_invariants<'genv>(
68    genv: GlobalEnv<'genv, '_>,
69    adt_def_id: MaybeExternId<OwnerId>,
70    params: &[fhir::RefineParam<'genv>],
71    invariants: &[fhir::Expr<'genv>],
72) -> Result<WfckResults> {
73    let owner = FluxOwnerId::Rust(adt_def_id);
74    let mut infcx = InferCtxt::new(genv, owner);
75    Wf::with(&mut infcx, |wf| {
76        wf.declare_params_for_invariants(params, invariants)?;
77
78        // Run first conv phase to gather sorts for associated refinements.
79        // This must run after declaring parameters because conversion expects
80        // the parameter sorts to be present in wfckresults.
81        wf.as_conv_ctxt()
82            .conv_invariants(adt_def_id.map(|it| it.def_id), params, invariants)
83            .emit(&wf.errors)?;
84
85        for invariant in invariants {
86            wf.check_expr(invariant, &rty::Sort::Bool);
87        }
88        Ok(())
89    })?;
90    infcx.into_results()
91}
92
93pub(crate) fn check_node<'genv>(
94    genv: GlobalEnv<'genv, '_>,
95    node: &fhir::OwnerNode<'genv>,
96) -> Result<WfckResults> {
97    let mut infcx = InferCtxt::new(genv, node.owner_id().into());
98    Wf::with(&mut infcx, |wf| {
99        wf.init_infcx_for_node(node)
100            .map_err(|err| err.at(genv.tcx().def_span(node.owner_id().local_id())))
101            .emit(&genv)?;
102
103        ImplicitParamInferer::infer(wf.infcx, node)?;
104
105        wf.check_node(node);
106        wf.check_hides_and_reveals(node.owner_id().local_id().def_id);
107        Ok(())
108    })?;
109
110    param_usage::check(&infcx, node)?;
111
112    infcx.into_results()
113}
114
115struct Wf<'a, 'genv, 'tcx> {
116    infcx: &'a mut InferCtxt<'genv, 'tcx>,
117    errors: Errors<'genv>,
118    next_type_index: u32,
119    next_region_index: u32,
120    next_const_index: u32,
121}
122
123impl<'a, 'genv, 'tcx> Wf<'a, 'genv, 'tcx> {
124    fn with(infcx: &'a mut InferCtxt<'genv, 'tcx>, f: impl FnOnce(&mut Self) -> Result) -> Result {
125        let errors = Errors::new(infcx.genv.sess());
126        let mut wf = Self {
127            infcx,
128            errors,
129            // We start sorts and types from 1 to skip the trait object dummy self type.
130            // See [`rty::Ty::trait_object_dummy_self`]
131            next_type_index: 1,
132            next_region_index: 0,
133            next_const_index: 0,
134        };
135        f(&mut wf)?;
136        wf.errors.into_result()
137    }
138
139    fn check_flux_item(&mut self, item: fhir::FluxItem<'genv>) {
140        self.visit_flux_item(&item);
141    }
142
143    fn check_node(&mut self, node: &fhir::OwnerNode<'genv>) {
144        self.visit_node(node);
145    }
146
147    /// Checks that `#[hide(...)]` and `#[reveal(...)]` have an effect. Hiding an inlined definition
148    /// or revealing an uninterpreted function are errors. Hiding an uninterpreted function or
149    /// revealing a definition that is not hidden by default are warnings.
150    fn check_hides_and_reveals(&mut self, def_id: LocalDefId) {
151        let genv = self.infcx.genv;
152        let attr_map = genv.fhir_attr_map(def_id);
153        for &(revealed, span) in attr_map.reveals {
154            match genv.spec_func(revealed) {
155                rty::SpecFunc::Uif => {
156                    self.errors
157                        .emit(errors::RevealUninterpretedFunction::new(span, revealed));
158                }
159                rty::SpecFunc::Defined { hide: false, .. } => {
160                    genv.sess()
161                        .dcx()
162                        .emit_warn(errors::RevealNotHiddenDefinition::new(span, revealed));
163                }
164                rty::SpecFunc::Defined { hide: true, .. } => {}
165            }
166        }
167        for &(hidden, span) in attr_map.hides {
168            if let rty::SpecFunc::Uif = genv.spec_func(hidden) {
169                genv.sess()
170                    .dcx()
171                    .emit_warn(errors::HideUninterpretedFunction::new(span, hidden));
172            } else if genv.should_inline_fun(hidden) {
173                self.errors
174                    .emit(errors::HideInlinedDefinition::new(span, hidden));
175            }
176            if attr_map
177                .reveals
178                .iter()
179                .any(|(revealed, _)| *revealed == hidden)
180            {
181                self.errors
182                    .emit(errors::HideAndRevealDefinition::new(span, hidden));
183            }
184        }
185    }
186
187    fn check_expr(&mut self, expr: &fhir::Expr<'genv>, sort: &rty::Sort) {
188        self.infcx
189            .check_expr(expr, sort)
190            .collect_err(&mut self.errors);
191    }
192
193    // We special-case primop applications to declare their parameters because their
194    // parameters are implicit from the underlying primop and must not be declared explicitly.
195    fn declare_params_for_primop_prop(&mut self, primop_prop: &fhir::PrimOpProp<'genv>) -> Result {
196        let Some((sorts, _)) = prim_op_sort(&primop_prop.op) else {
197            return Err(self
198                .errors
199                .emit(errors::UnsupportedPrimOp::new(primop_prop.span, primop_prop.op)));
200        };
201        if primop_prop.args.len() != sorts.len() {
202            return Err(self.errors.emit(errors::ArgCountMismatch::new(
203                Some(primop_prop.span),
204                String::from("primop"),
205                sorts.len(),
206                primop_prop.args.len(),
207            )));
208        }
209        for (arg, sort) in primop_prop.args.iter().zip(sorts) {
210            self.infcx.declare_param(*arg, sort);
211        }
212        visit_refine_params(
213            |vis| vis.visit_expr(&primop_prop.body),
214            |param| self.declare_param(param),
215        )
216    }
217
218    /// Recursively traverse `item` and declare all refinement parameters
219    fn declare_params_for_flux_item(&mut self, item: fhir::FluxItem<'genv>) -> Result {
220        if let fhir::FluxItem::PrimOpProp(primop_prop) = item {
221            self.declare_params_for_primop_prop(primop_prop)
222        } else {
223            visit_refine_params(|vis| vis.visit_flux_item(&item), |param| self.declare_param(param))
224        }
225    }
226
227    /// Recursively traverse `node` and declare all refinement parameters
228    fn declare_params_for_node(&mut self, node: &fhir::OwnerNode<'genv>) -> Result {
229        visit_refine_params(|vis| vis.visit_node(node), |param| self.declare_param(param))
230    }
231
232    /// Recursively traverse `invariants` and declare all refinement parameters
233    fn declare_params_for_invariants(
234        &mut self,
235        params: &[fhir::RefineParam<'genv>],
236        invariants: &[fhir::Expr<'genv>],
237    ) -> Result {
238        for param in params {
239            self.declare_param(param)?;
240        }
241        for expr in invariants {
242            self.declare_params_in_expr(expr)?;
243        }
244        Ok(())
245    }
246
247    fn declare_params_in_expr(&mut self, expr: &fhir::Expr<'genv>) -> Result {
248        visit_refine_params(|vis| vis.visit_expr(expr), |param| self.declare_param(param))
249    }
250
251    fn declare_param(&mut self, param: &fhir::RefineParam<'genv>) -> Result {
252        let sort = self
253            .as_conv_ctxt()
254            .conv_sort(&param.sort)
255            .emit(&self.genv())?;
256        self.infcx.declare_param(*param, sort);
257        Ok(())
258    }
259
260    /// To check for well-formedness we need to synthesize sorts for some nodes which is hard to
261    /// compute in `fhir`. For example, to check if the type `i32[e]` is well formed, we need to
262    /// know that the sort of `i32` is `int` so we can check the expression `e` against it. Computing
263    /// the sort from a base type is subtle and hard to do in `fhir` so we must do it in `rty`.
264    /// However, to convert from `fhir` to `rty` we need elaborated information from sort checking
265    /// which we do in `fhir`.
266    ///
267    /// To break this circularity, we do conversion in two phases. In the first phase, we do conversion
268    /// without elaborated information. This results in types in `rty` with incorrect refinements but
269    /// with the right *shape* to compute their sorts. We use these sorts for sort checking and then do
270    /// conversion again with the elaborated information.
271    ///
272    /// This function initializes the [inference context] by running the first phase of conversion and
273    /// collecting the sorts of some nodes that are hard to compute in `fhir`.
274    ///
275    /// [inference context]: InferCtxt
276    fn init_infcx_for_node(&mut self, node: &fhir::OwnerNode<'genv>) -> QueryResult {
277        let def_id = node.owner_id().map(|id| id.def_id);
278        self.declare_params_for_node(node)?;
279        let cx = self.as_conv_ctxt();
280        match node {
281            fhir::OwnerNode::Item(item) => {
282                match &item.kind {
283                    fhir::ItemKind::Enum(enum_def) => {
284                        cx.conv_enum_variants(def_id, enum_def)?;
285                        cx.conv_generic_predicates(def_id, &item.generics)?;
286                    }
287                    fhir::ItemKind::Struct(struct_def) => {
288                        cx.conv_struct_variant(def_id, struct_def)?;
289                        cx.conv_generic_predicates(def_id, &item.generics)?;
290                    }
291                    fhir::ItemKind::TyAlias(ty_alias) => {
292                        cx.conv_type_alias(def_id, ty_alias)?;
293                        cx.conv_generic_predicates(def_id, &item.generics)?;
294                    }
295                    fhir::ItemKind::Trait(trait_) => {
296                        for assoc_reft in trait_.assoc_refinements {
297                            if let Some(body) = assoc_reft.body {
298                                cx.conv_assoc_reft_body(
299                                    assoc_reft.params,
300                                    &body,
301                                    &assoc_reft.output,
302                                )?;
303                            }
304                        }
305                        cx.conv_generic_predicates(def_id, &item.generics)?;
306                    }
307                    fhir::ItemKind::Impl(impl_) => {
308                        for assoc_reft in impl_.assoc_refinements {
309                            cx.conv_assoc_reft_body(
310                                assoc_reft.params,
311                                &assoc_reft.body,
312                                &assoc_reft.output,
313                            )?;
314                        }
315                        cx.conv_generic_predicates(def_id, &item.generics)?;
316                    }
317                    fhir::ItemKind::Fn(fn_sig) => {
318                        cx.conv_fn_sig(def_id, fn_sig)?;
319                        cx.conv_generic_predicates(def_id, &item.generics)?;
320                    }
321                    fhir::ItemKind::Static(ty) => {
322                        if let Some(ty) = ty {
323                            cx.conv_static_ty(ty)?;
324                        }
325                    }
326                    fhir::ItemKind::Const(_) => {}
327                }
328            }
329            fhir::OwnerNode::TraitItem(trait_item) => {
330                match trait_item.kind {
331                    fhir::TraitItemKind::Fn(fn_sig) => {
332                        cx.conv_fn_sig(def_id, &fn_sig)?;
333                        cx.conv_generic_predicates(def_id, &trait_item.generics)?;
334                    }
335                    fhir::TraitItemKind::Type => {}
336                    fhir::TraitItemKind::Const => {}
337                }
338            }
339            fhir::OwnerNode::ImplItem(impl_item) => {
340                match impl_item.kind {
341                    fhir::ImplItemKind::Fn(fn_sig) => {
342                        cx.conv_fn_sig(def_id, &fn_sig)?;
343                        cx.conv_generic_predicates(def_id, &impl_item.generics)?;
344                    }
345                    fhir::ImplItemKind::Type => {}
346                    fhir::ImplItemKind::Const => {}
347                }
348            }
349            fhir::OwnerNode::ForeignItem(impl_item) => {
350                match impl_item.kind {
351                    fhir::ForeignItemKind::Fn(fn_sig, generics) => {
352                        cx.conv_fn_sig(def_id, &fn_sig)?;
353                        cx.conv_generic_predicates(def_id, generics)?;
354                    }
355                    fhir::ForeignItemKind::Static(_, _, _, _) => {
356                        // TODO: conv_ty if we want refinements on extern statics?
357                    }
358                }
359            }
360        }
361        self.infcx.normalize_sorts()
362    }
363
364    fn init_infcx_for_flux_item(&mut self, item: fhir::FluxItem<'genv>) -> QueryResult {
365        self.declare_params_for_flux_item(item)?;
366        let cx = self.as_conv_ctxt();
367        match item {
368            fhir::FluxItem::Qualifier(qualifier) => {
369                cx.conv_qualifier(qualifier)?;
370            }
371            fhir::FluxItem::Func(spec_func) => {
372                cx.conv_spec_func(spec_func)?;
373            }
374            fhir::FluxItem::PrimOpProp(prim_op_prop) => {
375                cx.conv_primop_prop(prim_op_prop)?;
376            }
377            fhir::FluxItem::Axiom(axiom) => {
378                cx.conv_axiom(axiom)?;
379            }
380            fhir::FluxItem::SortDecl(_sort_decl) => {}
381        }
382        Ok(())
383    }
384
385    fn check_output_locs(&mut self, fn_decl: &fhir::FnDecl) {
386        let mut output_locs = UnordSet::new();
387        for ens in fn_decl.output.ensures {
388            if let fhir::Ensures::Type(loc, ..) = ens
389                && let (_, id) = loc.res.expect_param()
390                && !output_locs.insert(id)
391            {
392                self.errors.emit(errors::DuplicatedEnsures::new(loc));
393            }
394        }
395
396        for ty in fn_decl.inputs {
397            if let fhir::TyKind::StrgRef(loc, _) = ty.kind
398                && let (_, id) = loc.res.expect_param()
399                && !output_locs.contains(&id)
400            {
401                self.errors.emit(errors::MissingEnsures::new(loc));
402            }
403        }
404    }
405}
406
407impl<'genv> fhir::visit::Visitor<'genv> for Wf<'_, 'genv, '_> {
408    fn visit_qualifier(&mut self, qual: &fhir::Qualifier<'genv>) {
409        self.check_expr(&qual.expr, &rty::Sort::Bool);
410
411        // A sort with no literals to scrape would silently make the qualifier inert.
412        let wildcards = std::iter::zip(qual.args, qual.wildcards)
413            .filter_map(|(param, &is_wildcard)| is_wildcard.then_some(param));
414        for param in wildcards {
415            let sort = self.infcx.param_sort(param.id);
416            if !matches!(
417                sort,
418                rty::Sort::Int | rty::Sort::Real | rty::Sort::Str | rty::Sort::BitVec(_)
419            ) {
420                self.errors
421                    .emit(errors::InvalidWildcardSort::new(param.span, sort));
422            }
423        }
424    }
425
426    fn visit_primop_prop(&mut self, primop_prop: &fhir::PrimOpProp<'genv>) {
427        let Some((sorts, _)) = prim_op_sort(&primop_prop.op) else {
428            self.errors
429                .emit(errors::UnsupportedPrimOp::new(primop_prop.span, primop_prop.op));
430            return;
431        };
432
433        if primop_prop.args.len() != sorts.len() {
434            self.errors.emit(errors::ArgCountMismatch::new(
435                Some(primop_prop.span),
436                String::from("primop"),
437                sorts.len(),
438                primop_prop.args.len(),
439            ));
440            return;
441        }
442        self.check_expr(&primop_prop.body, &rty::Sort::Bool);
443    }
444
445    fn visit_axiom(&mut self, axiom: &fhir::Axiom<'genv>) {
446        self.check_expr(&axiom.body, &rty::Sort::Bool);
447    }
448
449    fn visit_func(&mut self, func: &fhir::SpecFunc<'genv>) {
450        if let Some(body) = &func.body {
451            let Ok(output) = self.as_conv_ctxt().conv_sort(&func.sort).emit(&self.errors) else {
452                return;
453            };
454            self.check_expr(body, &output);
455        }
456    }
457
458    fn visit_impl_assoc_reft(&mut self, assoc_reft: &fhir::ImplAssocReft<'genv>) {
459        let Ok(output) = self
460            .as_conv_ctxt()
461            .conv_sort(&assoc_reft.output)
462            .emit(&self.errors)
463        else {
464            return;
465        };
466        self.check_expr(&assoc_reft.body, &output);
467    }
468
469    fn visit_trait_assoc_reft(&mut self, assoc_reft: &fhir::TraitAssocReft<'genv>) {
470        if let Some(body) = &assoc_reft.body {
471            let Ok(output) = self
472                .as_conv_ctxt()
473                .conv_sort(&assoc_reft.output)
474                .emit(&self.errors)
475            else {
476                return;
477            };
478            self.check_expr(body, &output);
479        }
480    }
481
482    fn visit_variant_ret(&mut self, ret: &fhir::VariantRet<'genv>) {
483        let genv = self.infcx.genv;
484        let enum_id = ret.enum_id;
485        let Ok(adt_sort_def) = genv.adt_sort_def_of(enum_id).emit(&self.errors) else { return };
486        if adt_sort_def.is_reflected() {
487            return;
488        }
489        let Ok(args) = rty::GenericArg::identity_for_item(genv, enum_id).emit(&self.errors) else {
490            return;
491        };
492        let expected = adt_sort_def.to_sort(&args);
493        self.check_expr(&ret.idx, &expected);
494    }
495
496    fn visit_fn_sig(&mut self, sig: &fhir::FnSig<'genv>) {
497        fhir::visit::walk_fn_sig(self, sig);
498        if let Some(e) = sig.no_panic_if {
499            self.check_expr(&e, &rty::Sort::Bool);
500        }
501    }
502
503    fn visit_fn_decl(&mut self, decl: &fhir::FnDecl<'genv>) {
504        fhir::visit::walk_fn_decl(self, decl);
505        self.check_output_locs(decl);
506    }
507
508    fn visit_requires(&mut self, requires: &fhir::Requires<'genv>) {
509        self.check_expr(&requires.pred, &rty::Sort::Bool);
510    }
511
512    fn visit_ensures(&mut self, ensures: &fhir::Ensures<'genv>) {
513        match ensures {
514            fhir::Ensures::Type(loc, ty) => {
515                self.infcx.check_loc(loc).collect_err(&mut self.errors);
516                self.visit_ty(ty);
517            }
518            fhir::Ensures::Pred(pred) => {
519                self.check_expr(pred, &rty::Sort::Bool);
520            }
521        }
522    }
523
524    fn visit_ty(&mut self, ty: &fhir::Ty<'genv>) {
525        match &ty.kind {
526            fhir::TyKind::Indexed(bty, idx) => {
527                let expected = self.infcx.sort_of_bty(bty);
528                self.check_expr(idx, &expected);
529                self.visit_bty(bty);
530            }
531            fhir::TyKind::StrgRef(loc, ty) => {
532                self.infcx.check_loc(loc).collect_err(&mut self.errors);
533                self.visit_ty(ty);
534            }
535            fhir::TyKind::Constr(pred, ty) => {
536                self.visit_ty(ty);
537                self.check_expr(pred, &rty::Sort::Bool);
538            }
539            _ => fhir::visit::walk_ty(self, ty),
540        }
541    }
542
543    fn visit_path(&mut self, path: &fhir::Path<'genv>) {
544        let genv = self.genv();
545        if let fhir::Res::Def(DefKind::TyAlias, def_id) = path.res {
546            let Ok(generics) = genv.refinement_generics_of(def_id).emit(&self.errors) else {
547                return;
548            };
549
550            let args = self.infcx.path_args(path.fhir_id);
551            for (i, expr) in path.refine.iter().enumerate() {
552                let Ok(param) = generics.param_at(i, genv).emit(&self.errors) else { return };
553                let param = param.instantiate(genv.tcx(), &args, &[]);
554                self.check_expr(expr, &param.sort);
555            }
556        };
557        fhir::visit::walk_path(self, path);
558    }
559}
560
561struct RefineParamVisitor<F> {
562    f: F,
563    err: Option<ErrorGuaranteed>,
564}
565
566impl<'v, F> fhir::visit::Visitor<'v> for RefineParamVisitor<F>
567where
568    F: FnMut(&fhir::RefineParam<'v>) -> Result,
569{
570    fn visit_refine_param(&mut self, param: &fhir::RefineParam<'v>) {
571        (self.f)(param).collect_err(&mut self.err);
572    }
573}
574
575fn visit_refine_params<'a, F>(visit: impl FnOnce(&mut RefineParamVisitor<F>), f: F) -> Result
576where
577    F: FnMut(&fhir::RefineParam<'a>) -> Result,
578{
579    let mut visitor = RefineParamVisitor { f, err: None };
580    visit(&mut visitor);
581    visitor.err.into_result()
582}
583
584impl<'genv, 'tcx> ConvPhase<'genv, 'tcx> for Wf<'_, 'genv, 'tcx> {
585    /// We don't expand type aliases before sort checking because we need every base type in `fhir`
586    /// to match a type in `rty`.
587    const EXPAND_TYPE_ALIASES: bool = false;
588    const HAS_ELABORATED_INFORMATION: bool = false;
589
590    type Results = InferCtxt<'genv, 'tcx>;
591
592    fn genv(&self) -> GlobalEnv<'genv, 'tcx> {
593        self.infcx.genv
594    }
595
596    fn owner(&self) -> FluxOwnerId {
597        self.infcx.wfckresults.owner
598    }
599
600    fn next_sort_vid(&mut self) -> rty::SortVid {
601        self.infcx.next_sort_vid(Default::default())
602    }
603
604    fn next_type_vid(&mut self) -> rty::TyVid {
605        self.next_type_index = self.next_type_index.checked_add(1).unwrap();
606        rty::TyVid::from_u32(self.next_type_index - 1)
607    }
608
609    fn next_region_vid(&mut self) -> rty::RegionVid {
610        self.next_region_index = self.next_region_index.checked_add(1).unwrap();
611        rty::RegionVid::from_u32(self.next_region_index - 1)
612    }
613
614    fn next_const_vid(&mut self) -> rty::ConstVid {
615        self.next_const_index = self.next_const_index.checked_add(1).unwrap();
616        rty::ConstVid::from_u32(self.next_const_index - 1)
617    }
618
619    fn results(&self) -> &Self::Results {
620        self.infcx
621    }
622
623    fn insert_node_sort(&mut self, fhir_id: FhirId, sort: rty::Sort) {
624        self.infcx.insert_node_sort(fhir_id, sort);
625    }
626
627    fn insert_path_args(&mut self, fhir_id: FhirId, args: rty::GenericArgs) {
628        self.infcx.insert_path_args(fhir_id, args);
629    }
630
631    fn insert_alias_reft_sort(&mut self, fhir_id: FhirId, fsort: rty::FuncSort) {
632        self.infcx.insert_sort_for_alias_reft(fhir_id, fsort);
633    }
634}
635
636/// The purpose of doing conversion before sort checking is to collect the sorts of base types.
637/// Thus, what we return here mostly doesn't matter because the refinements on a type should not
638/// affect its sort. The one exception is the sort we generate for refinement parameters.
639///
640/// For instance, consider the following definition where we refine a struct with a polymorphic set:
641/// ```ignore
642/// #[flux::refined_by(elems: Set<T>)]
643/// struct RSet<T> { ... }
644/// ```
645/// Now, consider the type `RSet<i32{v: v >= 0}>`. This type desugars to `RSet<λv:σ. {i32[v] | v >= 0}>`
646/// where the sort `σ` needs to be inferred. The type `RSet<λv:σ. {i32[v] | v >= 0}>` has sort
647/// `RSet<σ>` where `RSet` is the sort-level representation of the `RSet` type. Thus, it is important
648/// that the inference variable we generate for `σ` is the same we use for sort checking.
649impl WfckResultsProvider for InferCtxt<'_, '_> {
650    fn bin_op_sort(&self, _: FhirId) -> rty::Sort {
651        rty::Sort::Err
652    }
653
654    fn coercions_for(&self, _: FhirId) -> &[rty::Coercion] {
655        &[]
656    }
657
658    fn field_proj(&self, _: FhirId) -> rty::FieldProj {
659        rty::FieldProj::Tuple { arity: 0, field: 0 }
660    }
661
662    fn record_ctor(&self, _: FhirId) -> RecordCtor {
663        RecordCtor::Struct(DefId { index: DefIndex::from_u32(0), krate: CrateNum::from_u32(0) })
664    }
665
666    fn param_sort(&self, param_id: fhir::ParamId) -> rty::Sort {
667        self.param_sort(param_id)
668    }
669
670    fn node_sort(&self, _: FhirId) -> rty::Sort {
671        rty::Sort::Err
672    }
673
674    fn node_sort_args(&self, _: FhirId) -> rty::List<rty::SortArg> {
675        rty::List::empty()
676    }
677}
flux_fhir_analysis/wf/mod.rs

flux_fhir_analysis/wf/
mod.rs
