flux_refineck/
lib.rs

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

flux_refineck/
lib.rs
