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, WfckResults},
17};
18use rustc_errors::ErrorGuaranteed;
19use rustc_hash::FxHashSet;
20use rustc_hir::{
21    OwnerId,
22    def::DefKind,
23    def_id::{CrateNum, DefId, DefIndex},
24};
25
26use self::sortck::{ImplicitParamInferer, InferCtxt};
27use crate::conv::{ConvPhase, WfckResultsProvider};
28
29type Result<T = ()> = std::result::Result<T, ErrorGuaranteed>;
30
31pub(crate) fn check_flux_item<'genv>(
32    genv: GlobalEnv<'genv, '_>,
33    item: fhir::FluxItem<'genv>,
34) -> Result<WfckResults> {
35    let owner = FluxOwnerId::Flux(item.def_id());
36    let mut infcx = InferCtxt::new(genv, owner);
37    Wf::with(&mut infcx, |wf| {
38        wf.declare_params_for_flux_item(item)?;
39        wf.check_flux_item(item);
40        Ok(())
41    })?;
42    infcx.into_results()
43}
44
45pub(crate) fn check_constant_expr(
46    genv: GlobalEnv,
47    owner: OwnerId,
48    expr: &fhir::Expr,
49    sort: &rty::Sort,
50) -> Result<WfckResults> {
51    let mut infcx = InferCtxt::new(genv, FluxOwnerId::Rust(owner));
52    infcx.check_expr(expr, sort)?;
53    infcx.into_results()
54}
55
56pub(crate) fn check_invariants<'genv>(
57    genv: GlobalEnv<'genv, '_>,
58    adt_def_id: MaybeExternId<OwnerId>,
59    params: &[fhir::RefineParam<'genv>],
60    invariants: &[fhir::Expr<'genv>],
61) -> Result<WfckResults> {
62    let owner = FluxOwnerId::Rust(adt_def_id.local_id());
63    let mut infcx = InferCtxt::new(genv, owner);
64    Wf::with(&mut infcx, |wf| {
65        wf.declare_params_for_invariants(params, invariants)?;
66
67        // Run first conv phase to gather sorts for associated refinements.
68        // This must run after declaring parameters because conversion expects
69        // the parameter sorts to be present in wfckresults.
70        wf.as_conv_ctxt()
71            .conv_invariants(adt_def_id.map(|it| it.def_id), params, invariants)
72            .emit(&wf.errors)?;
73
74        for invariant in invariants {
75            wf.infcx
76                .check_expr(invariant, &rty::Sort::Bool)
77                .collect_err(&mut wf.errors);
78        }
79        Ok(())
80    })?;
81    infcx.into_results()
82}
83
84pub(crate) fn check_node<'genv>(
85    genv: GlobalEnv<'genv, '_>,
86    node: &fhir::OwnerNode<'genv>,
87) -> Result<WfckResults> {
88    let mut infcx = InferCtxt::new(genv, node.owner_id().local_id().into());
89    Wf::with(&mut infcx, |wf| {
90        wf.init_infcx(node)
91            .map_err(|err| err.at(genv.tcx().def_span(node.owner_id().local_id())))
92            .emit(&genv)?;
93
94        ImplicitParamInferer::infer(wf.infcx, node)?;
95
96        wf.check_node(node);
97        Ok(())
98    })?;
99
100    param_usage::check(&infcx, node)?;
101
102    infcx.into_results()
103}
104
105struct Wf<'a, 'genv, 'tcx> {
106    infcx: &'a mut InferCtxt<'genv, 'tcx>,
107    errors: Errors<'genv>,
108    next_type_index: u32,
109    next_region_index: u32,
110    next_const_index: u32,
111}
112
113impl<'a, 'genv, 'tcx> Wf<'a, 'genv, 'tcx> {
114    fn with(infcx: &'a mut InferCtxt<'genv, 'tcx>, f: impl FnOnce(&mut Self) -> Result) -> Result {
115        let errors = Errors::new(infcx.genv.sess());
116        let mut wf = Self {
117            infcx,
118            errors,
119            // We start sorts and types from 1 to skip the trait object dummy self type.
120            // See [`rty::Ty::trait_object_dummy_self`]
121            next_type_index: 1,
122            next_region_index: 0,
123            next_const_index: 0,
124        };
125        f(&mut wf)?;
126        wf.errors.into_result()
127    }
128
129    fn check_flux_item(&mut self, item: fhir::FluxItem<'genv>) {
130        self.visit_flux_item(&item);
131    }
132
133    fn check_node(&mut self, node: &fhir::OwnerNode<'genv>) {
134        self.visit_node(node);
135    }
136
137    /// Recursively traverse `item` and declare all refinement parameters
138    fn declare_params_for_flux_item(&mut self, item: fhir::FluxItem<'genv>) -> Result {
139        visit_refine_params(|vis| vis.visit_flux_item(&item), |param| self.declare_param(param))
140    }
141
142    /// Recursively traverse `node` and declare all refinement parameters
143    fn declare_params_for_node(&mut self, node: &fhir::OwnerNode<'genv>) -> Result {
144        visit_refine_params(|vis| vis.visit_node(node), |param| self.declare_param(param))
145    }
146
147    /// Recursively traverse `invariants` and declare all refinement parameters
148    fn declare_params_for_invariants(
149        &mut self,
150        params: &[fhir::RefineParam<'genv>],
151        invariants: &[fhir::Expr<'genv>],
152    ) -> Result {
153        for param in params {
154            self.declare_param(param)?;
155        }
156        for expr in invariants {
157            visit_refine_params(|vis| vis.visit_expr(expr), |param| self.declare_param(param))?;
158        }
159        Ok(())
160    }
161
162    fn declare_param(&mut self, param: &fhir::RefineParam<'genv>) -> Result {
163        let sort = self
164            .as_conv_ctxt()
165            .conv_sort(&param.sort)
166            .emit(&self.genv())?;
167        self.infcx.declare_param(*param, sort);
168        Ok(())
169    }
170
171    /// To check for well-formedness we need to know the sort of base types. For example, to check if
172    /// the type `i32[e]` is well formed, we need to know that the sort of `i32` is `int` so we can
173    /// check the expression `e` against it. Computing the sort from a base type is subtle and hard
174    /// to do in `fhir` so we must do it in `rty`. However, to convert from `fhir` to `rty` we need
175    /// elaborated information from sort checking which we do in `fhir`.
176    ///
177    /// To break this circularity, we do conversion in two phases. In the first phase, we do conversion
178    /// without elaborated information. This results in types in `rty` with incorrect refinements but
179    /// with the right *shape* to compute their sorts. We use these sorts for sort checking and then do
180    /// conversion again with the elaborated information.
181    ///
182    /// This function initializes the [inference context] by running the first phase of conversion and
183    /// collecting the sort of all base types.
184    ///
185    /// [inference context]: InferCtxt
186    fn init_infcx(&mut self, node: &fhir::OwnerNode<'genv>) -> QueryResult {
187        let def_id = node.owner_id().map(|id| id.def_id);
188        self.declare_params_for_node(node)?;
189        let cx = self.as_conv_ctxt();
190        match node {
191            fhir::OwnerNode::Item(item) => {
192                match &item.kind {
193                    fhir::ItemKind::Enum(enum_def) => {
194                        cx.conv_enum_variants(def_id, enum_def)?;
195                        cx.conv_generic_predicates(def_id, &item.generics)?;
196                    }
197                    fhir::ItemKind::Struct(struct_def) => {
198                        cx.conv_struct_variant(def_id, struct_def)?;
199                        cx.conv_generic_predicates(def_id, &item.generics)?;
200                    }
201                    fhir::ItemKind::TyAlias(ty_alias) => {
202                        cx.conv_type_alias(def_id, ty_alias)?;
203                        cx.conv_generic_predicates(def_id, &item.generics)?;
204                    }
205                    fhir::ItemKind::Trait(trait_) => {
206                        for assoc_reft in trait_.assoc_refinements {
207                            if let Some(body) = assoc_reft.body {
208                                cx.conv_assoc_reft_body(
209                                    assoc_reft.params,
210                                    &body,
211                                    &assoc_reft.output,
212                                )?;
213                            }
214                        }
215                        cx.conv_generic_predicates(def_id, &item.generics)?;
216                    }
217                    fhir::ItemKind::Impl(impl_) => {
218                        for assoc_reft in impl_.assoc_refinements {
219                            cx.conv_assoc_reft_body(
220                                assoc_reft.params,
221                                &assoc_reft.body,
222                                &assoc_reft.output,
223                            )?;
224                        }
225                        cx.conv_generic_predicates(def_id, &item.generics)?;
226                    }
227                    fhir::ItemKind::Fn(fn_sig) => {
228                        cx.conv_fn_sig(def_id, fn_sig)?;
229                        cx.conv_generic_predicates(def_id, &item.generics)?;
230                    }
231                    fhir::ItemKind::Const(_) => {}
232                }
233            }
234            fhir::OwnerNode::TraitItem(trait_item) => {
235                match trait_item.kind {
236                    fhir::TraitItemKind::Fn(fn_sig) => {
237                        cx.conv_fn_sig(def_id, &fn_sig)?;
238                        cx.conv_generic_predicates(def_id, &trait_item.generics)?;
239                    }
240                    fhir::TraitItemKind::Type => {}
241                    fhir::TraitItemKind::Const => {}
242                }
243            }
244            fhir::OwnerNode::ImplItem(impl_item) => {
245                match impl_item.kind {
246                    fhir::ImplItemKind::Fn(fn_sig) => {
247                        cx.conv_fn_sig(def_id, &fn_sig)?;
248                        cx.conv_generic_predicates(def_id, &impl_item.generics)?;
249                    }
250                    fhir::ImplItemKind::Type => {}
251                    fhir::ImplItemKind::Const => {}
252                }
253            }
254            fhir::OwnerNode::ForeignItem(impl_item) => {
255                match impl_item.kind {
256                    fhir::ForeignItemKind::Fn(fn_sig, generics) => {
257                        cx.conv_fn_sig(def_id, &fn_sig)?;
258                        cx.conv_generic_predicates(def_id, generics)?;
259                    }
260                }
261            }
262        }
263        self.infcx.normalize_sorts()
264    }
265
266    fn check_output_locs(&mut self, fn_decl: &fhir::FnDecl) {
267        let mut output_locs = FxHashSet::default();
268        for ens in fn_decl.output.ensures {
269            if let fhir::Ensures::Type(loc, ..) = ens
270                && let (_, id) = loc.res.expect_param()
271                && !output_locs.insert(id)
272            {
273                self.errors.emit(errors::DuplicatedEnsures::new(loc));
274            }
275        }
276
277        for ty in fn_decl.inputs {
278            if let fhir::TyKind::StrgRef(_, loc, _) = ty.kind
279                && let (_, id) = loc.res.expect_param()
280                && !output_locs.contains(&id)
281            {
282                self.errors.emit(errors::MissingEnsures::new(loc));
283            }
284        }
285    }
286}
287
288impl<'genv> fhir::visit::Visitor<'genv> for Wf<'_, 'genv, '_> {
289    fn visit_qualifier(&mut self, qual: &fhir::Qualifier<'genv>) {
290        self.infcx
291            .check_expr(&qual.expr, &rty::Sort::Bool)
292            .collect_err(&mut self.errors);
293    }
294
295    fn visit_func(&mut self, func: &fhir::SpecFunc<'genv>) {
296        if let Some(body) = &func.body {
297            let Ok(output) = self.as_conv_ctxt().conv_sort(&func.sort).emit(&self.errors) else {
298                return;
299            };
300            self.infcx
301                .check_expr(body, &output)
302                .collect_err(&mut self.errors);
303        }
304    }
305
306    fn visit_impl_assoc_reft(&mut self, assoc_reft: &fhir::ImplAssocReft) {
307        let Ok(output) = self
308            .as_conv_ctxt()
309            .conv_sort(&assoc_reft.output)
310            .emit(&self.errors)
311        else {
312            return;
313        };
314        self.infcx
315            .check_expr(&assoc_reft.body, &output)
316            .collect_err(&mut self.errors);
317    }
318
319    fn visit_trait_assoc_reft(&mut self, assoc_reft: &fhir::TraitAssocReft) {
320        if let Some(body) = &assoc_reft.body {
321            let Ok(output) = self
322                .as_conv_ctxt()
323                .conv_sort(&assoc_reft.output)
324                .emit(&self.errors)
325            else {
326                return;
327            };
328            self.infcx
329                .check_expr(body, &output)
330                .collect_err(&mut self.errors);
331        }
332    }
333
334    fn visit_variant_ret(&mut self, ret: &fhir::VariantRet) {
335        let genv = self.infcx.genv;
336        let enum_id = ret.enum_id;
337        let Ok(adt_sort_def) = genv.adt_sort_def_of(enum_id).emit(&self.errors) else { return };
338        if adt_sort_def.is_reflected() {
339            return;
340        }
341        let Ok(args) = rty::GenericArg::identity_for_item(genv, enum_id).emit(&self.errors) else {
342            return;
343        };
344        let expected = adt_sort_def.to_sort(&args);
345        self.infcx
346            .check_expr(&ret.idx, &expected)
347            .collect_err(&mut self.errors);
348    }
349
350    fn visit_fn_decl(&mut self, decl: &fhir::FnDecl<'genv>) {
351        fhir::visit::walk_fn_decl(self, decl);
352        self.check_output_locs(decl);
353    }
354
355    fn visit_requires(&mut self, requires: &fhir::Requires<'genv>) {
356        self.infcx
357            .check_expr(&requires.pred, &rty::Sort::Bool)
358            .collect_err(&mut self.errors);
359    }
360
361    fn visit_ensures(&mut self, ensures: &fhir::Ensures<'genv>) {
362        match ensures {
363            fhir::Ensures::Type(loc, ty) => {
364                self.infcx.check_loc(loc).collect_err(&mut self.errors);
365                self.visit_ty(ty);
366            }
367            fhir::Ensures::Pred(pred) => {
368                self.infcx
369                    .check_expr(pred, &rty::Sort::Bool)
370                    .collect_err(&mut self.errors);
371            }
372        }
373    }
374
375    fn visit_ty(&mut self, ty: &fhir::Ty<'genv>) {
376        match &ty.kind {
377            fhir::TyKind::Indexed(bty, idx) => {
378                let expected = self.infcx.sort_of_bty(bty.fhir_id);
379                self.infcx
380                    .check_expr(idx, &expected)
381                    .collect_err(&mut self.errors);
382                self.visit_bty(bty);
383            }
384            fhir::TyKind::StrgRef(_, loc, ty) => {
385                self.infcx.check_loc(loc).collect_err(&mut self.errors);
386                self.visit_ty(ty);
387            }
388            fhir::TyKind::Constr(pred, ty) => {
389                self.visit_ty(ty);
390                self.infcx
391                    .check_expr(pred, &rty::Sort::Bool)
392                    .collect_err(&mut self.errors);
393            }
394            _ => fhir::visit::walk_ty(self, ty),
395        }
396    }
397
398    fn visit_path(&mut self, path: &fhir::Path<'genv>) {
399        let genv = self.genv();
400        if let fhir::Res::Def(DefKind::TyAlias, def_id) = path.res {
401            let Ok(generics) = genv.refinement_generics_of(def_id).emit(&self.errors) else {
402                return;
403            };
404
405            let args = self.infcx.path_args(path.fhir_id);
406            for (i, expr) in path.refine.iter().enumerate() {
407                let Ok(param) = generics.param_at(i, genv).emit(&self.errors) else { return };
408                let param = param.instantiate(genv.tcx(), &args, &[]);
409                self.infcx
410                    .check_expr(expr, &param.sort)
411                    .collect_err(&mut self.errors);
412            }
413        };
414        fhir::visit::walk_path(self, path);
415    }
416}
417
418struct RefineParamVisitor<F> {
419    f: F,
420    err: Option<ErrorGuaranteed>,
421}
422
423impl<'v, F> fhir::visit::Visitor<'v> for RefineParamVisitor<F>
424where
425    F: FnMut(&fhir::RefineParam<'v>) -> Result,
426{
427    fn visit_refine_param(&mut self, param: &fhir::RefineParam<'v>) {
428        (self.f)(param).collect_err(&mut self.err);
429    }
430}
431
432fn visit_refine_params<'a, F>(visit: impl FnOnce(&mut RefineParamVisitor<F>), f: F) -> Result
433where
434    F: FnMut(&fhir::RefineParam<'a>) -> Result,
435{
436    let mut visitor = RefineParamVisitor { f, err: None };
437    visit(&mut visitor);
438    visitor.err.into_result()
439}
440
441impl<'genv, 'tcx> ConvPhase<'genv, 'tcx> for Wf<'_, 'genv, 'tcx> {
442    /// We don't expand type aliases before sort checking because we need every base type in `fhir`
443    /// to match a type in `rty`.
444    const EXPAND_TYPE_ALIASES: bool = false;
445    const HAS_ELABORATED_INFORMATION: bool = false;
446
447    type Results = InferCtxt<'genv, 'tcx>;
448
449    fn genv(&self) -> GlobalEnv<'genv, 'tcx> {
450        self.infcx.genv
451    }
452
453    fn owner(&self) -> FluxOwnerId {
454        self.infcx.wfckresults.owner
455    }
456
457    fn next_sort_vid(&mut self) -> rty::SortVid {
458        self.infcx.next_sort_vid()
459    }
460
461    fn next_type_vid(&mut self) -> rty::TyVid {
462        self.next_type_index = self.next_type_index.checked_add(1).unwrap();
463        rty::TyVid::from_u32(self.next_type_index - 1)
464    }
465
466    fn next_region_vid(&mut self) -> rty::RegionVid {
467        self.next_region_index = self.next_region_index.checked_add(1).unwrap();
468        rty::RegionVid::from_u32(self.next_region_index - 1)
469    }
470
471    fn next_const_vid(&mut self) -> rty::ConstVid {
472        self.next_const_index = self.next_const_index.checked_add(1).unwrap();
473        rty::ConstVid::from_u32(self.next_const_index - 1)
474    }
475
476    fn results(&self) -> &Self::Results {
477        self.infcx
478    }
479
480    fn insert_bty_sort(&mut self, fhir_id: FhirId, sort: rty::Sort) {
481        self.infcx.insert_sort_for_bty(fhir_id, sort);
482    }
483
484    fn insert_path_args(&mut self, fhir_id: FhirId, args: rty::GenericArgs) {
485        self.infcx.insert_path_args(fhir_id, args);
486    }
487
488    fn insert_alias_reft_sort(&mut self, fhir_id: FhirId, fsort: rty::FuncSort) {
489        self.infcx.insert_sort_for_alias_reft(fhir_id, fsort);
490    }
491}
492
493/// The purpose of doing conversion before sort checking is to collect the sorts of base types.
494/// Thus, what we return here mostly doesn't matter because the refinements on a type should not
495/// affect its sort. The one exception is the sort we generate for refinement parameters.
496///
497/// For instance, consider the following definition where we refine a struct with a polymorphic set:
498/// ```ignore
499/// #[flux::refined_by(elems: Set<T>)]
500/// struct RSet<T> { ... }
501/// ```
502/// Now, consider the type `RSet<i32{v: v >= 0}>`. This type desugars to `RSet<λv:σ. {i32[v] | v >= 0}>`
503/// where the sort `σ` needs to be inferred. The type `RSet<λv:σ. {i32[v] | v >= 0}>` has sort
504/// `RSet<σ>` where `RSet` is the sort-level representation of the `RSet` type. Thus, it is important
505/// that the inference variable we generate for `σ` is the same we use for sort checking.
506impl WfckResultsProvider for InferCtxt<'_, '_> {
507    fn bin_op_sort(&self, _: FhirId) -> rty::Sort {
508        rty::Sort::Err
509    }
510
511    fn coercions_for(&self, _: FhirId) -> &[rty::Coercion] {
512        &[]
513    }
514
515    fn field_proj(&self, _: FhirId) -> rty::FieldProj {
516        rty::FieldProj::Tuple { arity: 0, field: 0 }
517    }
518
519    fn record_ctor(&self, _: FhirId) -> DefId {
520        DefId { index: DefIndex::from_u32(0), krate: CrateNum::from_u32(0) }
521    }
522
523    fn param_sort(&self, param: &fhir::RefineParam) -> rty::Sort {
524        self.param_sort(param.id)
525    }
526
527    fn node_sort(&self, _: FhirId) -> rty::Sort {
528        rty::Sort::Err
529    }
530}
flux_fhir_analysis/wf/mod.rs

flux_fhir_analysis/wf/
mod.rs
