1mod 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::{
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: 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.local_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 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().local_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 Ok(())
107 })?;
108
109 param_usage::check(&infcx, node)?;
110
111 infcx.into_results()
112}
113
114struct Wf<'a, 'genv, 'tcx> {
115 infcx: &'a mut InferCtxt<'genv, 'tcx>,
116 errors: Errors<'genv>,
117 next_type_index: u32,
118 next_region_index: u32,
119 next_const_index: u32,
120}
121
122impl<'a, 'genv, 'tcx> Wf<'a, 'genv, 'tcx> {
123 fn with(infcx: &'a mut InferCtxt<'genv, 'tcx>, f: impl FnOnce(&mut Self) -> Result) -> Result {
124 let errors = Errors::new(infcx.genv.sess());
125 let mut wf = Self {
126 infcx,
127 errors,
128 next_type_index: 1,
131 next_region_index: 0,
132 next_const_index: 0,
133 };
134 f(&mut wf)?;
135 wf.errors.into_result()
136 }
137
138 fn check_flux_item(&mut self, item: fhir::FluxItem<'genv>) {
139 self.visit_flux_item(&item);
140 }
141
142 fn check_node(&mut self, node: &fhir::OwnerNode<'genv>) {
143 self.visit_node(node);
144 }
145
146 fn check_expr(&mut self, expr: &fhir::Expr<'genv>, sort: &rty::Sort) {
147 self.infcx
148 .check_expr(expr, sort)
149 .collect_err(&mut self.errors);
150 }
151
152 fn declare_params_for_primop_prop(&mut self, primop_prop: &fhir::PrimOpProp<'genv>) -> Result {
155 let Some((sorts, _)) = prim_op_sort(&primop_prop.op) else {
156 return Err(self
157 .errors
158 .emit(errors::UnsupportedPrimOp::new(primop_prop.span, primop_prop.op)));
159 };
160 if primop_prop.args.len() != sorts.len() {
161 return Err(self.errors.emit(errors::ArgCountMismatch::new(
162 Some(primop_prop.span),
163 String::from("primop"),
164 sorts.len(),
165 primop_prop.args.len(),
166 )));
167 }
168 for (arg, sort) in primop_prop.args.iter().zip(sorts) {
169 self.infcx.declare_param(*arg, sort);
170 }
171 visit_refine_params(
172 |vis| vis.visit_expr(&primop_prop.body),
173 |param| self.declare_param(param),
174 )
175 }
176
177 fn declare_params_for_flux_item(&mut self, item: fhir::FluxItem<'genv>) -> Result {
179 if let fhir::FluxItem::PrimOpProp(primop_prop) = item {
180 self.declare_params_for_primop_prop(primop_prop)
181 } else {
182 visit_refine_params(|vis| vis.visit_flux_item(&item), |param| self.declare_param(param))
183 }
184 }
185
186 fn declare_params_for_node(&mut self, node: &fhir::OwnerNode<'genv>) -> Result {
188 visit_refine_params(|vis| vis.visit_node(node), |param| self.declare_param(param))
189 }
190
191 fn declare_params_for_invariants(
193 &mut self,
194 params: &[fhir::RefineParam<'genv>],
195 invariants: &[fhir::Expr<'genv>],
196 ) -> Result {
197 for param in params {
198 self.declare_param(param)?;
199 }
200 for expr in invariants {
201 self.declare_params_in_expr(expr)?;
202 }
203 Ok(())
204 }
205
206 fn declare_params_in_expr(&mut self, expr: &fhir::Expr<'genv>) -> Result {
207 visit_refine_params(|vis| vis.visit_expr(expr), |param| self.declare_param(param))
208 }
209
210 fn declare_param(&mut self, param: &fhir::RefineParam<'genv>) -> Result {
211 let sort = self
212 .as_conv_ctxt()
213 .conv_sort(¶m.sort)
214 .emit(&self.genv())?;
215 self.infcx.declare_param(*param, sort);
216 Ok(())
217 }
218
219 fn init_infcx_for_node(&mut self, node: &fhir::OwnerNode<'genv>) -> QueryResult {
236 let def_id = node.owner_id().map(|id| id.def_id);
237 self.declare_params_for_node(node)?;
238 let cx = self.as_conv_ctxt();
239 match node {
240 fhir::OwnerNode::Item(item) => {
241 match &item.kind {
242 fhir::ItemKind::Enum(enum_def) => {
243 cx.conv_enum_variants(def_id, enum_def)?;
244 cx.conv_generic_predicates(def_id, &item.generics)?;
245 }
246 fhir::ItemKind::Struct(struct_def) => {
247 cx.conv_struct_variant(def_id, struct_def)?;
248 cx.conv_generic_predicates(def_id, &item.generics)?;
249 }
250 fhir::ItemKind::TyAlias(ty_alias) => {
251 cx.conv_type_alias(def_id, ty_alias)?;
252 cx.conv_generic_predicates(def_id, &item.generics)?;
253 }
254 fhir::ItemKind::Trait(trait_) => {
255 for assoc_reft in trait_.assoc_refinements {
256 if let Some(body) = assoc_reft.body {
257 cx.conv_assoc_reft_body(
258 assoc_reft.params,
259 &body,
260 &assoc_reft.output,
261 )?;
262 }
263 }
264 cx.conv_generic_predicates(def_id, &item.generics)?;
265 }
266 fhir::ItemKind::Impl(impl_) => {
267 for assoc_reft in impl_.assoc_refinements {
268 cx.conv_assoc_reft_body(
269 assoc_reft.params,
270 &assoc_reft.body,
271 &assoc_reft.output,
272 )?;
273 }
274 cx.conv_generic_predicates(def_id, &item.generics)?;
275 }
276 fhir::ItemKind::Fn(fn_sig) => {
277 cx.conv_fn_sig(def_id, fn_sig)?;
278 cx.conv_generic_predicates(def_id, &item.generics)?;
279 }
280 fhir::ItemKind::Const(_) => {}
281 }
282 }
283 fhir::OwnerNode::TraitItem(trait_item) => {
284 match trait_item.kind {
285 fhir::TraitItemKind::Fn(fn_sig) => {
286 cx.conv_fn_sig(def_id, &fn_sig)?;
287 cx.conv_generic_predicates(def_id, &trait_item.generics)?;
288 }
289 fhir::TraitItemKind::Type => {}
290 fhir::TraitItemKind::Const => {}
291 }
292 }
293 fhir::OwnerNode::ImplItem(impl_item) => {
294 match impl_item.kind {
295 fhir::ImplItemKind::Fn(fn_sig) => {
296 cx.conv_fn_sig(def_id, &fn_sig)?;
297 cx.conv_generic_predicates(def_id, &impl_item.generics)?;
298 }
299 fhir::ImplItemKind::Type => {}
300 fhir::ImplItemKind::Const => {}
301 }
302 }
303 fhir::OwnerNode::ForeignItem(impl_item) => {
304 match impl_item.kind {
305 fhir::ForeignItemKind::Fn(fn_sig, generics) => {
306 cx.conv_fn_sig(def_id, &fn_sig)?;
307 cx.conv_generic_predicates(def_id, generics)?;
308 }
309 }
310 }
311 }
312 self.infcx.normalize_sorts()
313 }
314
315 fn init_infcx_for_flux_item(&mut self, item: fhir::FluxItem<'genv>) -> QueryResult {
316 self.declare_params_for_flux_item(item)?;
317 let cx = self.as_conv_ctxt();
318 match item {
319 fhir::FluxItem::Qualifier(qualifier) => {
320 cx.conv_qualifier(qualifier)?;
321 }
322 fhir::FluxItem::Func(spec_func) => {
323 cx.conv_defn(spec_func)?;
324 }
325 fhir::FluxItem::PrimOpProp(prim_op_prop) => {
326 cx.conv_primop_prop(prim_op_prop)?;
327 }
328 }
329 Ok(())
330 }
331
332 fn check_output_locs(&mut self, fn_decl: &fhir::FnDecl) {
333 let mut output_locs = FxHashSet::default();
334 for ens in fn_decl.output.ensures {
335 if let fhir::Ensures::Type(loc, ..) = ens
336 && let (_, id) = loc.res.expect_param()
337 && !output_locs.insert(id)
338 {
339 self.errors.emit(errors::DuplicatedEnsures::new(loc));
340 }
341 }
342
343 for ty in fn_decl.inputs {
344 if let fhir::TyKind::StrgRef(_, loc, _) = ty.kind
345 && let (_, id) = loc.res.expect_param()
346 && !output_locs.contains(&id)
347 {
348 self.errors.emit(errors::MissingEnsures::new(loc));
349 }
350 }
351 }
352}
353
354impl<'genv> fhir::visit::Visitor<'genv> for Wf<'_, 'genv, '_> {
355 fn visit_qualifier(&mut self, qual: &fhir::Qualifier<'genv>) {
356 self.check_expr(&qual.expr, &rty::Sort::Bool);
357 }
358
359 fn visit_primop_prop(&mut self, primop_prop: &fhir::PrimOpProp<'genv>) {
360 let Some((sorts, _)) = prim_op_sort(&primop_prop.op) else {
361 self.errors
362 .emit(errors::UnsupportedPrimOp::new(primop_prop.span, primop_prop.op));
363 return;
364 };
365
366 if primop_prop.args.len() != sorts.len() {
367 self.errors.emit(errors::ArgCountMismatch::new(
368 Some(primop_prop.span),
369 String::from("primop"),
370 sorts.len(),
371 primop_prop.args.len(),
372 ));
373 return;
374 }
375 self.check_expr(&primop_prop.body, &rty::Sort::Bool);
376 }
377
378 fn visit_func(&mut self, func: &fhir::SpecFunc<'genv>) {
379 if let Some(body) = &func.body {
380 let Ok(output) = self.as_conv_ctxt().conv_sort(&func.sort).emit(&self.errors) else {
381 return;
382 };
383 self.check_expr(body, &output);
384 }
385 }
386
387 fn visit_impl_assoc_reft(&mut self, assoc_reft: &fhir::ImplAssocReft<'genv>) {
388 let Ok(output) = self
389 .as_conv_ctxt()
390 .conv_sort(&assoc_reft.output)
391 .emit(&self.errors)
392 else {
393 return;
394 };
395 self.check_expr(&assoc_reft.body, &output);
396 }
397
398 fn visit_trait_assoc_reft(&mut self, assoc_reft: &fhir::TraitAssocReft<'genv>) {
399 if let Some(body) = &assoc_reft.body {
400 let Ok(output) = self
401 .as_conv_ctxt()
402 .conv_sort(&assoc_reft.output)
403 .emit(&self.errors)
404 else {
405 return;
406 };
407 self.check_expr(body, &output);
408 }
409 }
410
411 fn visit_variant_ret(&mut self, ret: &fhir::VariantRet<'genv>) {
412 let genv = self.infcx.genv;
413 let enum_id = ret.enum_id;
414 let Ok(adt_sort_def) = genv.adt_sort_def_of(enum_id).emit(&self.errors) else { return };
415 if adt_sort_def.is_reflected() {
416 return;
417 }
418 let Ok(args) = rty::GenericArg::identity_for_item(genv, enum_id).emit(&self.errors) else {
419 return;
420 };
421 let expected = adt_sort_def.to_sort(&args);
422 self.check_expr(&ret.idx, &expected);
423 }
424
425 fn visit_fn_decl(&mut self, decl: &fhir::FnDecl<'genv>) {
426 fhir::visit::walk_fn_decl(self, decl);
427 self.check_output_locs(decl);
428 }
429
430 fn visit_requires(&mut self, requires: &fhir::Requires<'genv>) {
431 self.check_expr(&requires.pred, &rty::Sort::Bool);
432 }
433
434 fn visit_ensures(&mut self, ensures: &fhir::Ensures<'genv>) {
435 match ensures {
436 fhir::Ensures::Type(loc, ty) => {
437 self.infcx.check_loc(loc).collect_err(&mut self.errors);
438 self.visit_ty(ty);
439 }
440 fhir::Ensures::Pred(pred) => {
441 self.check_expr(pred, &rty::Sort::Bool);
442 }
443 }
444 }
445
446 fn visit_ty(&mut self, ty: &fhir::Ty<'genv>) {
447 match &ty.kind {
448 fhir::TyKind::Indexed(bty, idx) => {
449 let expected = self.infcx.sort_of_bty(bty);
450 self.check_expr(idx, &expected);
451 self.visit_bty(bty);
452 }
453 fhir::TyKind::StrgRef(_, loc, ty) => {
454 self.infcx.check_loc(loc).collect_err(&mut self.errors);
455 self.visit_ty(ty);
456 }
457 fhir::TyKind::Constr(pred, ty) => {
458 self.visit_ty(ty);
459 self.check_expr(pred, &rty::Sort::Bool);
460 }
461 _ => fhir::visit::walk_ty(self, ty),
462 }
463 }
464
465 fn visit_path(&mut self, path: &fhir::Path<'genv>) {
466 let genv = self.genv();
467 if let fhir::Res::Def(DefKind::TyAlias, def_id) = path.res {
468 let Ok(generics) = genv.refinement_generics_of(def_id).emit(&self.errors) else {
469 return;
470 };
471
472 let args = self.infcx.path_args(path.fhir_id);
473 for (i, expr) in path.refine.iter().enumerate() {
474 let Ok(param) = generics.param_at(i, genv).emit(&self.errors) else { return };
475 let param = param.instantiate(genv.tcx(), &args, &[]);
476 self.check_expr(expr, ¶m.sort);
477 }
478 };
479 fhir::visit::walk_path(self, path);
480 }
481}
482
483struct RefineParamVisitor<F> {
484 f: F,
485 err: Option<ErrorGuaranteed>,
486}
487
488impl<'v, F> fhir::visit::Visitor<'v> for RefineParamVisitor<F>
489where
490 F: FnMut(&fhir::RefineParam<'v>) -> Result,
491{
492 fn visit_refine_param(&mut self, param: &fhir::RefineParam<'v>) {
493 (self.f)(param).collect_err(&mut self.err);
494 }
495}
496
497fn visit_refine_params<'a, F>(visit: impl FnOnce(&mut RefineParamVisitor<F>), f: F) -> Result
498where
499 F: FnMut(&fhir::RefineParam<'a>) -> Result,
500{
501 let mut visitor = RefineParamVisitor { f, err: None };
502 visit(&mut visitor);
503 visitor.err.into_result()
504}
505
506impl<'genv, 'tcx> ConvPhase<'genv, 'tcx> for Wf<'_, 'genv, 'tcx> {
507 const EXPAND_TYPE_ALIASES: bool = false;
510 const HAS_ELABORATED_INFORMATION: bool = false;
511
512 type Results = InferCtxt<'genv, 'tcx>;
513
514 fn genv(&self) -> GlobalEnv<'genv, 'tcx> {
515 self.infcx.genv
516 }
517
518 fn owner(&self) -> FluxOwnerId {
519 self.infcx.wfckresults.owner
520 }
521
522 fn next_sort_vid(&mut self) -> rty::SortVid {
523 self.infcx.next_sort_vid()
524 }
525
526 fn next_type_vid(&mut self) -> rty::TyVid {
527 self.next_type_index = self.next_type_index.checked_add(1).unwrap();
528 rty::TyVid::from_u32(self.next_type_index - 1)
529 }
530
531 fn next_region_vid(&mut self) -> rty::RegionVid {
532 self.next_region_index = self.next_region_index.checked_add(1).unwrap();
533 rty::RegionVid::from_u32(self.next_region_index - 1)
534 }
535
536 fn next_const_vid(&mut self) -> rty::ConstVid {
537 self.next_const_index = self.next_const_index.checked_add(1).unwrap();
538 rty::ConstVid::from_u32(self.next_const_index - 1)
539 }
540
541 fn results(&self) -> &Self::Results {
542 self.infcx
543 }
544
545 fn insert_node_sort(&mut self, fhir_id: FhirId, sort: rty::Sort) {
546 self.infcx.insert_node_sort(fhir_id, sort);
547 }
548
549 fn insert_path_args(&mut self, fhir_id: FhirId, args: rty::GenericArgs) {
550 self.infcx.insert_path_args(fhir_id, args);
551 }
552
553 fn insert_alias_reft_sort(&mut self, fhir_id: FhirId, fsort: rty::FuncSort) {
554 self.infcx.insert_sort_for_alias_reft(fhir_id, fsort);
555 }
556}
557
558impl WfckResultsProvider for InferCtxt<'_, '_> {
572 fn bin_op_sort(&self, _: FhirId) -> rty::Sort {
573 rty::Sort::Err
574 }
575
576 fn coercions_for(&self, _: FhirId) -> &[rty::Coercion] {
577 &[]
578 }
579
580 fn field_proj(&self, _: FhirId) -> rty::FieldProj {
581 rty::FieldProj::Tuple { arity: 0, field: 0 }
582 }
583
584 fn record_ctor(&self, _: FhirId) -> DefId {
585 DefId { index: DefIndex::from_u32(0), krate: CrateNum::from_u32(0) }
586 }
587
588 fn param_sort(&self, param_id: fhir::ParamId) -> rty::Sort {
589 self.param_sort(param_id)
590 }
591
592 fn node_sort(&self, _: FhirId) -> rty::Sort {
593 rty::Sort::Err
594 }
595
596 fn node_sort_args(&self, _: FhirId) -> rty::List<rty::SortArg> {
597 rty::List::empty()
598 }
599}