1#![feature(
4 associated_type_defaults,
5 box_patterns,
6 if_let_guard,
7 min_specialization,
8 never_type,
9 rustc_private,
10 unwrap_infallible
11)]
12
13extern crate rustc_abi;
14extern crate rustc_data_structures;
15extern crate rustc_errors;
16extern crate rustc_hir;
17extern crate rustc_index;
18extern crate rustc_infer;
19extern crate rustc_middle;
20extern crate rustc_mir_dataflow;
21extern crate rustc_span;
22extern crate rustc_type_ir;
23
24mod checker;
25pub mod compare_impl_item;
26mod ghost_statements;
27pub mod invariants;
28mod primops;
29mod queue;
30mod type_env;
31
32use checker::{Checker, trait_impl_subtyping};
33use flux_common::{dbg, dbg::SpanTrace, result::ResultExt as _};
34use flux_config as config;
35use flux_infer::{
36 fixpoint_encoding::{
37 FixQueryCache, FixpointCheckError, PossibleSolutions, SolutionTrace, TagIdx,
38 },
39 infer::{ConstrReason, SubtypeReason, Tag},
40 wkvars::WKVarSubst,
41};
42use flux_macros::fluent_messages;
43use flux_middle::{
44 FixpointQueryKind,
45 def_id::MaybeExternId,
46 global_env::GlobalEnv,
47 metrics::{self, Metric, TimingKind},
48 pretty,
49 rty::{self, ESpan, EarlyBinder, fold::TypeFoldable},
50};
51use rustc_data_structures::{fx::FxHashMap, unord::UnordMap};
52use rustc_errors::{Applicability, Diag, ErrorGuaranteed};
53use rustc_hir::def_id::{DefId, LocalDefId};
54use rustc_span::Span;
55
56use crate::{checker::errors::ResultExt as _, ghost_statements::compute_ghost_statements};
57
58fluent_messages! { "../locales/en-US.ftl" }
59
60pub fn report_fixpoint_errors(
61 genv: GlobalEnv,
62 local_id: LocalDefId,
63 errors: Vec<FixpointCheckError<Tag>>,
64) -> Result<(), ErrorGuaranteed> {
65 #[expect(clippy::collapsible_else_if, reason = "it looks better")]
66 if genv.should_fail(local_id) {
67 if errors.is_empty() { report_expected_neg(genv, local_id) } else { Ok(()) }
68 } else {
69 if errors.is_empty() { Ok(()) } else { report_errors(genv, local_id, errors) }
70 }
71}
72
73fn check_body(
74 genv: GlobalEnv,
75 cache: &mut FixQueryCache,
76 def_id: LocalDefId,
77 poly_sig: &rty::PolyFnSig,
78) -> Result<(), ErrorGuaranteed> {
79 let span = genv.tcx().def_span(def_id);
80 let opts = genv.infer_opts(def_id);
81
82 dbg::log_verbose!("FLUX checking: {def_id:?} {span:?}");
83
84 let ghost_stmts = compute_ghost_statements(genv, def_id)
85 .with_span(span)
86 .map_err(|err| err.emit(genv, def_id))?;
87 let mut closures = UnordMap::default();
88
89 let shape_result =
91 Checker::run_in_shape_mode(genv, def_id, &ghost_stmts, &mut closures, opts, poly_sig)
92 .map_err(|err| err.emit(genv, def_id))?;
93
94 let infcx_root = Checker::run_in_refine_mode(
96 genv,
97 def_id,
98 &ghost_stmts,
99 &mut closures,
100 shape_result,
101 opts,
102 poly_sig,
103 )
104 .map_err(|err| err.emit(genv, def_id))?;
105
106 if (genv.proven_externally(def_id).is_some() && flux_config::lean().is_check())
108 || flux_config::lean().is_emit()
109 {
110 infcx_root
111 .execute_lean_query(cache, MaybeExternId::Local(def_id))
112 .emit(&genv)
113 } else {
114 let answer = infcx_root
115 .execute_fixpoint_query(cache, MaybeExternId::Local(def_id), FixpointQueryKind::Body)
116 .emit(&genv)?;
117
118 let tcx = genv.tcx();
119 let hir_id = tcx.local_def_id_to_hir_id(def_id);
120 let body_span = tcx.hir_span_with_body(hir_id);
121 dbg::solution!(genv, &answer, body_span);
122
123 let errors = answer.errors;
124 report_fixpoint_errors(genv, def_id, errors)
125 }
126}
127
128pub fn check_static(
129 genv: GlobalEnv,
130 cache: &mut FixQueryCache,
131 def_id: LocalDefId,
132 ty: rty::Ty,
133) -> Result<(), ErrorGuaranteed> {
134 let output = rty::Binder::dummy(rty::FnOutput::new(ty, vec![]));
136 let fn_sig = rty::FnSig::new(
137 rustc_hir::Safety::Safe,
138 rustc_abi::ExternAbi::Rust,
139 rty::List::empty(),
140 rty::List::empty(),
141 output,
142 rty::Expr::ff(),
143 false,
144 );
145 let poly_sig = rty::PolyFnSig::dummy(fn_sig);
146
147 metrics::incr_metric(Metric::FnChecked, 1);
148 metrics::time_it(TimingKind::CheckBody(def_id), || check_body(genv, cache, def_id, &poly_sig))
149}
150
151pub fn check_fn(
152 genv: GlobalEnv,
153 cache: &mut FixQueryCache,
154 def_id: LocalDefId,
155) -> Result<(), ErrorGuaranteed> {
156 let span = genv.tcx().def_span(def_id);
157
158 if span.in_derive_expansion()
163 && let Some(adt_def_id) = genv.derive_self_ty(def_id)
164 && genv.trusted_derive(adt_def_id)
165 {
166 metrics::incr_metric(Metric::FnTrusted, 1);
167 return Ok(());
168 }
169
170 let opts = genv.infer_opts(def_id);
171
172 if let Some(infcx_root) = trait_impl_subtyping(genv, def_id, opts, span)
174 .with_span(span)
175 .map_err(|err| err.emit(genv, def_id))?
176 {
177 tracing::info!("check_fn::refine-subtyping");
178 let answer = infcx_root
179 .execute_fixpoint_query(cache, MaybeExternId::Local(def_id), FixpointQueryKind::Impl)
180 .emit(&genv)?;
181 tracing::info!("check_fn::fixpoint-subtyping");
182 let errors = answer.errors;
183 report_fixpoint_errors(genv, def_id, errors)?;
184 }
185
186 if genv.trusted(def_id) {
188 metrics::incr_metric(Metric::FnTrusted, 1);
189 return Ok(());
190 }
191
192 metrics::incr_metric(Metric::FnChecked, 1);
193 metrics::time_it(TimingKind::CheckBody(def_id), || -> Result<(), ErrorGuaranteed> {
194 let poly_sig = genv
195 .fn_sig(def_id)
196 .with_span(span)
197 .map_err(|err| err.emit(genv, def_id))?
198 .instantiate_identity();
199 let poly_sig = rty::auto_strong(genv, def_id, poly_sig);
200
201 check_body(genv, cache, def_id, &poly_sig)
202 })?;
203
204 dbg::check_fn_span!(genv.tcx(), def_id).in_scope(|| Ok(()))
205}
206
207fn call_error<'a>(genv: GlobalEnv<'a, '_>, span: Span, dst_span: Option<ESpan>) -> Diag<'a> {
208 genv.sess()
209 .dcx()
210 .handle()
211 .create_err(errors::RefineError::call(span, dst_span))
212}
213
214fn ret_error<'a>(genv: GlobalEnv<'a, '_>, span: Span, dst_span: Option<ESpan>) -> Diag<'a> {
215 genv.sess()
216 .dcx()
217 .handle()
218 .create_err(errors::RefineError::ret(span, dst_span))
219}
220
221fn report_errors(
222 genv: GlobalEnv,
223 local_id: LocalDefId,
224 errors: Vec<FixpointCheckError<Tag>>,
225) -> Result<(), ErrorGuaranteed> {
226 let log_path = if config::dump_constraint() {
227 let path = dbg::item_dump_path(genv.tcx(), local_id.to_def_id(), "smt2");
228 if path.exists() { Some(path) } else { None }
229 } else {
230 None
231 };
232 let mut solutions_by_tag: FxHashMap<Tag, (TagIdx, PossibleSolutions)> = FxHashMap::default();
233 for error in errors {
234 if let Some((_, val)) = solutions_by_tag.get_mut(&error.tag) {
235 val.extend(error.possible_solutions);
236 } else {
237 solutions_by_tag.insert(error.tag, (error.tag_idx, error.possible_solutions));
238 }
239 }
240 let rerun_note = rerun_hint_note(genv, local_id);
241 let mut e = None;
242 for (tag, (tag_idx, possible_solutions)) in solutions_by_tag {
243 let span = tag.src_span;
244 let mut err_diag = match tag.reason {
245 ConstrReason::Call
246 | ConstrReason::Subtype(SubtypeReason::Input)
247 | ConstrReason::Subtype(SubtypeReason::Requires)
248 | ConstrReason::Predicate => call_error(genv, span, tag.dst_span),
249 ConstrReason::Assign => {
250 genv.sess()
251 .dcx()
252 .handle()
253 .create_err(errors::AssignError { span })
254 }
255 ConstrReason::Ret
256 | ConstrReason::Subtype(SubtypeReason::Output)
257 | ConstrReason::Subtype(SubtypeReason::Ensures) => ret_error(genv, span, tag.dst_span),
258 ConstrReason::Div => {
259 genv.sess()
260 .dcx()
261 .handle()
262 .create_err(errors::DivError { span })
263 }
264 ConstrReason::Rem => {
265 genv.sess()
266 .dcx()
267 .handle()
268 .create_err(errors::RemError { span })
269 }
270 ConstrReason::Goto(_) => {
271 genv.sess()
272 .dcx()
273 .handle()
274 .create_err(errors::GotoError { span })
275 }
276 ConstrReason::Assert(msg) => {
277 genv.sess()
278 .dcx()
279 .handle()
280 .create_err(errors::AssertError { span, msg })
281 }
282 ConstrReason::Fold | ConstrReason::FoldLocal => {
283 genv.sess()
284 .dcx()
285 .handle()
286 .create_err(errors::FoldError::new(span, tag.dst_span))
287 }
288 ConstrReason::Overflow => {
289 genv.sess()
290 .dcx()
291 .handle()
292 .create_err(errors::OverflowError { span })
293 }
294 ConstrReason::Underflow => {
295 genv.sess()
296 .dcx()
297 .handle()
298 .create_err(errors::UnderflowError { span })
299 }
300 ConstrReason::Other => {
301 genv.sess()
302 .dcx()
303 .handle()
304 .create_err(errors::UnknownError { span })
305 }
306 ConstrReason::NoPanic(callee, reason) => {
307 genv.sess().dcx().handle().create_err(errors::PanicError {
308 span,
309 callee: genv.tcx().def_path_debug_str(callee),
310 reason: format!("{:?}", reason),
311 })
312 }
313 };
314 let wkvar_solutions = possible_solutions
315 .iter()
316 .flat_map(|(wkvid, solutions)| solutions.iter().map(move |solution| (wkvid, solution)));
317 for (wkvid, solution) in wkvar_solutions {
318 add_fn_fix_diagnostic(genv, &mut err_diag, wkvid.clone(), solution);
319 }
320 if let Some(note) = &rerun_note {
321 err_diag.note(note.clone());
322 }
323 if let Some(path) = &log_path {
324 err_diag.arg("path", path.display().to_string());
325 err_diag.arg("tag", tag_idx.to_string());
326 err_diag.note(crate::fluent_generated::refineck_constraint_log_note);
327 }
328 e = Some(err_diag.emit());
329 }
330
331 if let Some(e) = e { Err(e) } else { Ok(()) }
332}
333
334fn report_expected_neg(genv: GlobalEnv, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
335 Err(genv.sess().emit_err(errors::ExpectedNeg {
336 span: genv.tcx().def_span(def_id),
337 def_descr: genv.tcx().def_descr(def_id.to_def_id()),
338 }))
339}
340
341fn add_fn_fix_diagnostic<'a>(
342 genv: GlobalEnv<'a, '_>,
343 diag: &mut Diag<'a>,
344 wkvid: rty::WKVid,
345 solution: &rty::Binder<rty::Expr>,
346) {
347 let pretty_solution = solution.map_ref(|e| e.simplify(&Default::default()).prettify());
348 let fn_sig = genv.fn_sig(wkvid.parent_fn).unwrap();
349 let mut wkvar_subst = WKVarSubst::new(
350 std::iter::once((wkvid.clone(), pretty_solution)).collect::<UnordMap<_, _>>(),
351 false,
352 );
353 let solved_fn_sig = EarlyBinder(fn_sig.skip_binder_ref().fold_with(&mut wkvar_subst));
354 let fixed_fn_sig_snippet = format!(
355 "{:?}",
356 pretty::with_cx!(&pretty::PrettyCx::default(genv).hide_regions(true), &solved_fn_sig)
357 );
358 let fn_first_line = fn_first_line(genv, wkvid.parent_fn);
359 let fn_first_line_snippet = genv
360 .tcx()
361 .sess
362 .source_map()
363 .span_to_snippet(fn_first_line)
364 .unwrap_or_else(|_| panic!("No snippet for span {:?}", fn_first_line));
365 let prefix_spaces = &fn_first_line_snippet[..fn_first_line_snippet
366 .find(|c: char| !c.is_whitespace())
367 .unwrap_or(fn_first_line_snippet.len())];
368 let subst_solutions = &wkvar_subst.subst_instantiations[&wkvid];
369 assert!(subst_solutions.len() == 1);
370
371 if let Some(old_spec_span) = genv.spec_attr_span(wkvid.parent_fn) {
373 diag.span_suggestion(
374 old_spec_span,
375 "try replacing the refinement",
376 format!("{}#[flux_rs::sig({})]", prefix_spaces, fixed_fn_sig_snippet),
377 Applicability::MachineApplicable,
378 );
379 } else {
380 diag.span_suggestion(
381 fn_first_line,
382 "try adding the refinement",
383 format!(
384 "{}#[flux_rs::sig({})]\n{}",
385 prefix_spaces, fixed_fn_sig_snippet, fn_first_line_snippet
386 ),
387 Applicability::MachineApplicable,
388 );
389 }
390}
391
392fn fn_first_line<'a>(genv: GlobalEnv<'a, '_>, def_id: DefId) -> Span {
393 let span = genv.tcx().def_span(def_id);
394 let first_line = genv
395 .tcx()
396 .sess
397 .source_map()
398 .lookup_line(span.lo())
399 .unwrap_or_else(|_| panic!("span for {:?} doesn't have a first line", def_id));
400 let first_line_range = first_line.sf.line_bounds(first_line.line);
401 Span::new(first_line_range.start, first_line_range.end, span.ctxt(), None)
402}
403
404fn rerun_hint_note(genv: GlobalEnv, def_id: LocalDefId) -> Option<String> {
405 if !config::rerun_hint() || !config::inside_cargo() {
406 return None;
407 }
408 let pattern = format!("def:{}", genv.tcx().def_path_str(def_id));
409 let pkg = std::env::var("CARGO_PKG_NAME")
410 .map(|p| format!(" -p {p}"))
411 .unwrap_or_default();
412 Some(format!("to rerun: `cargo flux check{pkg} --only-check={}`", shell_quote_arg(&pattern)))
413}
414
415fn shell_quote_arg(arg: &str) -> String {
416 format!("'{}'", arg.replace('\'', "'\\''"))
417}
418
419mod errors {
420 use flux_errors::E0999;
421 use flux_macros::{Diagnostic, Subdiagnostic};
422 use flux_middle::rty::ESpan;
423 use rustc_span::Span;
424
425 #[derive(Diagnostic)]
426 #[diag(refineck_goto_error, code = E0999)]
427 pub struct GotoError {
428 #[primary_span]
429 pub span: Span,
430 }
431
432 #[derive(Diagnostic)]
433 #[diag(refineck_assign_error, code = E0999)]
434 pub struct AssignError {
435 #[primary_span]
436 pub span: Span,
437 }
438
439 #[derive(Subdiagnostic)]
440 #[note(refineck_condition_span_note)]
441 pub(crate) struct ConditionSpanNote {
442 #[primary_span]
443 pub span: Span,
444 }
445
446 #[derive(Subdiagnostic)]
447 #[note(refineck_call_span_note)]
448 pub(crate) struct CallSpanNote {
449 #[primary_span]
450 pub span: Span,
451 }
452
453 #[derive(Diagnostic)]
454 #[diag(refineck_refine_error, code = E0999)]
455 pub struct RefineError {
456 #[primary_span]
457 #[label]
458 pub span: Span,
459 cond: &'static str,
460 #[subdiagnostic]
461 span_note: Option<ConditionSpanNote>,
462 #[subdiagnostic]
463 call_span_note: Option<CallSpanNote>,
464 }
465
466 impl RefineError {
467 pub fn call(span: Span, espan: Option<ESpan>) -> Self {
468 RefineError::new("precondition", span, espan)
469 }
470
471 pub fn ret(span: Span, espan: Option<ESpan>) -> Self {
472 RefineError::new("postcondition", span, espan)
473 }
474
475 fn new(cond: &'static str, span: Span, espan: Option<ESpan>) -> RefineError {
476 match espan {
477 Some(dst_span) => {
478 let span_note = Some(ConditionSpanNote { span: dst_span.span });
479 let call_span_note = dst_span.base.map(|span| CallSpanNote { span });
480 RefineError { span, cond, span_note, call_span_note }
481 }
482 None => RefineError { span, cond, span_note: None, call_span_note: None },
483 }
484 }
485 }
486
487 #[derive(Diagnostic)]
488 #[diag(refineck_div_error, code = E0999)]
489 pub struct DivError {
490 #[primary_span]
491 pub span: Span,
492 }
493
494 #[derive(Diagnostic)]
495 #[diag(refineck_rem_error, code = E0999)]
496 pub struct RemError {
497 #[primary_span]
498 pub span: Span,
499 }
500
501 #[derive(Diagnostic)]
502 #[diag(refineck_assert_error, code = E0999)]
503 pub struct AssertError {
504 #[primary_span]
505 pub span: Span,
506 pub msg: &'static str,
507 }
508
509 #[derive(Diagnostic)]
510 #[diag(refineck_fold_error, code = E0999)]
511 pub struct FoldError {
512 #[primary_span]
513 pub span: Span,
514 #[subdiagnostic]
515 span_note: Option<ConditionSpanNote>,
516 }
517
518 impl FoldError {
519 pub fn new(span: Span, espan: Option<ESpan>) -> Self {
520 let span_note = espan.map(|espan| ConditionSpanNote { span: espan.span });
521 FoldError { span, span_note }
522 }
523 }
524
525 #[derive(Diagnostic)]
526 #[diag(refineck_overflow_error, code = E0999)]
527 pub struct OverflowError {
528 #[primary_span]
529 pub span: Span,
530 }
531
532 #[derive(Diagnostic)]
533 #[diag(refineck_underflow_error, code = E0999)]
534 pub struct UnderflowError {
535 #[primary_span]
536 pub span: Span,
537 }
538
539 #[derive(Diagnostic)]
540 #[diag(refineck_unknown_error, code = E0999)]
541 pub struct UnknownError {
542 #[primary_span]
543 pub span: Span,
544 }
545
546 #[derive(Diagnostic)]
547 #[diag(refineck_expected_neg, code = E0999)]
548 pub struct ExpectedNeg {
549 #[primary_span]
550 pub span: Span,
551 pub def_descr: &'static str,
552 }
553
554 #[derive(Diagnostic)]
555 #[diag(refineck_panic_error, code = E0999)]
556 pub(super) struct PanicError {
557 #[primary_span]
558 pub(super) span: Span,
559 pub(super) callee: String,
560 pub(super) reason: String,
561 }
562}