flux_fhir_analysis/wf/
param_usage.rs

1//! Code to check whether refinement parameters are used in allowed positions.
2//!
3//! The correct usage of a parameter depends on whether its infer mode is [evar] or [kvar].
4//! For evar mode, parameters must be used at least once as an index in a position that fully
5//! determines their value (see <https://arxiv.org/pdf/2209.13000.pdf> for details). Parameters
6//! with kvar mode (i.e., abstract refinement predicates) must only be used in function position
7//! in a top-level conjunction such that they result in a proper horn constraint after being
8//! substituted by a kvar as required by fixpoint.
9//!
10//! [evar]: `fhir::InferMode::EVar`
11//! [kvar]: `fhir::InferMode::KVar`
12
13use flux_errors::Errors;
14use flux_middle::{
15    fhir::{self, visit::Visitor},
16    rty, walk_list,
17};
18use rustc_data_structures::snapshot_map;
19use rustc_span::ErrorGuaranteed;
20
21use super::{
22    errors::{InvalidParamPos, ParamNotDetermined},
23    sortck::InferCtxt,
24};
25
26type Result<T = ()> = std::result::Result<T, ErrorGuaranteed>;
27
28pub(crate) fn check<'genv>(infcx: &InferCtxt<'genv, '_>, node: &fhir::OwnerNode<'genv>) -> Result {
29    ParamUsesChecker::new(infcx).run(|ck| ck.visit_node(node))
30}
31
32struct ParamUsesChecker<'a, 'genv, 'tcx> {
33    infcx: &'a InferCtxt<'genv, 'tcx>,
34    /// Keeps track of all refinement parameters that are used as an index such that their value is fully
35    /// determined. The name xi is taken from [1], where the well-formedness judgment uses an uppercase
36    /// Xi (Ξ) for a context that is similar in purpose.
37    ///
38    /// This is basically a set of [`fhir::ParamId`] implemented with a snapshot map such that elements
39    /// can be removed in batch when there's a change in polarity.
40    ///
41    /// [1]: https://arxiv.org/pdf/2209.13000.pdf
42    xi: snapshot_map::SnapshotMap<fhir::ParamId, ()>,
43    errors: Errors<'genv>,
44}
45
46impl<'a, 'genv, 'tcx> ParamUsesChecker<'a, 'genv, 'tcx> {
47    fn new(infcx: &'a InferCtxt<'genv, 'tcx>) -> Self {
48        Self { infcx, xi: Default::default(), errors: Errors::new(infcx.genv.sess()) }
49    }
50
51    fn run(mut self, f: impl FnOnce(&mut Self)) -> Result {
52        f(&mut self);
53        self.errors.into_result()
54    }
55
56    /// Insert params that are considered to be value determined to `xi`.
57    fn insert_value_determined(&mut self, expr: &fhir::Expr) {
58        match expr.kind {
59            fhir::ExprKind::Var(path, _) if let fhir::ExprRes::Param(_, id) = path.res => {
60                self.xi.insert(id, ());
61            }
62            fhir::ExprKind::Record(fields) => {
63                for field in fields {
64                    self.insert_value_determined(field);
65                }
66            }
67            fhir::ExprKind::Constructor(_, fields, _) => {
68                for field in fields {
69                    self.insert_value_determined(&field.expr);
70                }
71            }
72            _ => {}
73        }
74    }
75
76    /// Checks that refinement parameters of function sort are used in allowed positions.
77    fn check_func_params_uses(&mut self, expr: &fhir::Expr, is_top_level_conj: bool) {
78        match expr.kind {
79            fhir::ExprKind::BinaryOp(bin_op, e1, e2) => {
80                let is_top_level_conj = is_top_level_conj && matches!(bin_op, fhir::BinOp::And);
81                self.check_func_params_uses(e1, is_top_level_conj);
82                self.check_func_params_uses(e2, is_top_level_conj);
83            }
84            fhir::ExprKind::UnaryOp(_, e) => self.check_func_params_uses(e, false),
85            fhir::ExprKind::App(func, args) => {
86                if !is_top_level_conj
87                    && let fhir::ExprRes::Param(_, id) = func.res
88                    && let fhir::InferMode::KVar = self.infcx.infer_mode(id)
89                {
90                    self.errors
91                        .emit(InvalidParamPos::new(func.span, &self.infcx.param_sort(id)));
92                }
93                for arg in args {
94                    self.check_func_params_uses(arg, false);
95                }
96            }
97            fhir::ExprKind::Alias(_, func_args) => {
98                // TODO(nilehmann) should we check the usage inside the `AliasPred`?
99                for arg in func_args {
100                    self.check_func_params_uses(arg, false);
101                }
102            }
103            fhir::ExprKind::Var(var, _) => {
104                if let fhir::ExprRes::Param(_, id) = var.res
105                    && let sort @ rty::Sort::Func(_) = self.infcx.param_sort(id)
106                {
107                    self.errors.emit(InvalidParamPos::new(var.span, &sort));
108                }
109            }
110            fhir::ExprKind::IfThenElse(e1, e2, e3) => {
111                self.check_func_params_uses(e1, false);
112                self.check_func_params_uses(e3, false);
113                self.check_func_params_uses(e2, false);
114            }
115            fhir::ExprKind::Literal(_) => {}
116            fhir::ExprKind::Dot(base, _) => {
117                self.check_func_params_uses(base, false);
118            }
119            fhir::ExprKind::Abs(_, body) => {
120                self.check_func_params_uses(body, true);
121            }
122            fhir::ExprKind::BoundedQuant(_, _, _, body) => {
123                self.check_func_params_uses(body, false);
124            }
125            fhir::ExprKind::Record(fields) => {
126                for field in fields {
127                    self.check_func_params_uses(field, is_top_level_conj);
128                }
129            }
130            fhir::ExprKind::Constructor(_, fields, spread) => {
131                if let Some(spread) = spread {
132                    self.check_func_params_uses(&spread.expr, false);
133                }
134                for field in fields {
135                    self.check_func_params_uses(&field.expr, false);
136                }
137            }
138            fhir::ExprKind::Block(decls, body) => {
139                for decl in decls {
140                    self.check_func_params_uses(&decl.init, false);
141                }
142                self.check_func_params_uses(body, false);
143            }
144            fhir::ExprKind::Err(_) => {
145                // an error has already been reported so we can just skip
146            }
147        }
148    }
149
150    /// Check that Hindly parameters in `params` appear in a value determined position
151    fn check_params_are_value_determined(&mut self, params: &[fhir::RefineParam]) {
152        for param in params {
153            let determined = self.xi.remove(param.id);
154            if self.infcx.infer_mode(param.id) == fhir::InferMode::EVar && !determined {
155                self.errors
156                    .emit(ParamNotDetermined::new(param.span, param.name));
157            }
158        }
159    }
160}
161
162impl<'genv> fhir::visit::Visitor<'genv> for ParamUsesChecker<'_, 'genv, '_> {
163    fn visit_node(&mut self, node: &fhir::OwnerNode<'genv>) {
164        if node.fn_sig().is_some() {
165            // Check early refinement parameters in fn-like nodes
166            let snapshot = self.xi.snapshot();
167            fhir::visit::walk_node(self, node);
168            self.check_params_are_value_determined(node.generics().refinement_params);
169            self.xi.rollback_to(snapshot);
170        } else {
171            fhir::visit::walk_node(self, node);
172        }
173    }
174
175    fn visit_ty_alias(&mut self, ty_alias: &fhir::TyAlias<'genv>) {
176        fhir::visit::walk_ty_alias(self, ty_alias);
177        self.check_params_are_value_determined(ty_alias.index.as_slice());
178    }
179
180    fn visit_struct_def(&mut self, struct_def: &fhir::StructDef<'genv>) {
181        if let fhir::StructKind::Transparent { fields } = struct_def.kind {
182            walk_list!(self, visit_field_def, fields);
183            self.check_params_are_value_determined(struct_def.params);
184        }
185    }
186
187    fn visit_variant(&mut self, variant: &fhir::VariantDef<'genv>) {
188        let snapshot = self.xi.snapshot();
189        fhir::visit::walk_variant(self, variant);
190        self.check_params_are_value_determined(variant.params);
191        self.xi.rollback_to(snapshot);
192    }
193
194    fn visit_variant_ret(&mut self, ret: &fhir::VariantRet<'genv>) {
195        let snapshot = self.xi.snapshot();
196        fhir::visit::walk_variant_ret(self, ret);
197        self.xi.rollback_to(snapshot);
198    }
199
200    fn visit_fn_output(&mut self, output: &fhir::FnOutput<'genv>) {
201        let snapshot = self.xi.snapshot();
202        fhir::visit::walk_fn_output(self, output);
203        self.check_params_are_value_determined(output.params);
204        self.xi.rollback_to(snapshot);
205    }
206
207    fn visit_ty(&mut self, ty: &fhir::Ty<'genv>) {
208        match &ty.kind {
209            fhir::TyKind::StrgRef(_, loc, ty) => {
210                let (_, id) = loc.res.expect_param();
211                self.xi.insert(id, ());
212                self.visit_ty(ty);
213            }
214            fhir::TyKind::Exists(params, ty) => {
215                self.visit_ty(ty);
216                self.check_params_are_value_determined(params);
217            }
218            fhir::TyKind::Indexed(bty, expr) => {
219                fhir::visit::walk_bty(self, bty);
220                self.insert_value_determined(expr);
221                self.check_func_params_uses(expr, false);
222            }
223            _ => fhir::visit::walk_ty(self, ty),
224        }
225    }
226
227    fn visit_expr(&mut self, expr: &fhir::Expr) {
228        self.check_func_params_uses(expr, true);
229    }
230
231    fn visit_path_segment(&mut self, segment: &fhir::PathSegment<'genv>) {
232        let is_box = self.infcx.genv.is_box(segment.res);
233
234        for (i, arg) in segment.args.iter().enumerate() {
235            let snapshot = self.xi.snapshot();
236            self.visit_generic_arg(arg);
237            if !(is_box && i == 0) {
238                self.xi.rollback_to(snapshot);
239            }
240        }
241        walk_list!(self, visit_assoc_item_constraint, segment.constraints);
242    }
243}
flux_fhir_analysis/wf/param_usage.rs

flux_fhir_analysis/wf/
param_usage.rs
