flux_refineck/
lib.rs

1//! Refinement type checking
2
3#![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::{FixQueryCache, SolutionTrace, TagIdx},
37    infer::{ConstrReason, SubtypeReason, Tag},
38};
39use flux_macros::fluent_messages;
40use flux_middle::{
41    FixpointQueryKind,
42    def_id::MaybeExternId,
43    global_env::GlobalEnv,
44    metrics::{self, Metric, TimingKind},
45    rty::{self},
46};
47use rustc_data_structures::unord::UnordMap;
48use rustc_errors::{Diagnostic as _, ErrorGuaranteed};
49use rustc_hir::def_id::LocalDefId;
50
51use crate::{checker::errors::ResultExt as _, ghost_statements::compute_ghost_statements};
52
53fluent_messages! { "../locales/en-US.ftl" }
54
55fn report_fixpoint_errors(
56    genv: GlobalEnv,
57    local_id: LocalDefId,
58    errors: Vec<(Tag, TagIdx)>,
59) -> Result<(), ErrorGuaranteed> {
60    #[expect(clippy::collapsible_else_if, reason = "it looks better")]
61    if genv.should_fail(local_id) {
62        if errors.is_empty() { report_expected_neg(genv, local_id) } else { Ok(()) }
63    } else {
64        if errors.is_empty() { Ok(()) } else { report_errors(genv, local_id, errors) }
65    }
66}
67
68fn check_body(
69    genv: GlobalEnv,
70    cache: &mut FixQueryCache,
71    def_id: LocalDefId,
72    poly_sig: &rty::PolyFnSig,
73) -> Result<(), ErrorGuaranteed> {
74    let span = genv.tcx().def_span(def_id);
75    let opts = genv.infer_opts(def_id);
76
77    dbg::log_verbose!("FLUX checking: {def_id:?} {span:?}");
78
79    let ghost_stmts = compute_ghost_statements(genv, def_id)
80        .with_span(span)
81        .map_err(|err| err.emit(genv, def_id))?;
82    let mut closures = UnordMap::default();
83
84    // PHASE 1: infer shape of `TypeEnv` at the entry of join points
85    let shape_result =
86        Checker::run_in_shape_mode(genv, def_id, &ghost_stmts, &mut closures, opts, poly_sig)
87            .map_err(|err| err.emit(genv, def_id))?;
88
89    // PHASE 2: generate refinement tree constraint
90    let infcx_root = Checker::run_in_refine_mode(
91        genv,
92        def_id,
93        &ghost_stmts,
94        &mut closures,
95        shape_result,
96        opts,
97        poly_sig,
98    )
99    .map_err(|err| err.emit(genv, def_id))?;
100
101    // PHASE 3: invoke fixpoint on the constraint
102    if (genv.proven_externally(def_id).is_some() && flux_config::lean().is_check())
103        || flux_config::lean().is_emit()
104    {
105        infcx_root
106            .execute_lean_query(cache, MaybeExternId::Local(def_id))
107            .emit(&genv)
108    } else {
109        let answer = infcx_root
110            .execute_fixpoint_query(cache, MaybeExternId::Local(def_id), FixpointQueryKind::Body)
111            .emit(&genv)?;
112
113        let tcx = genv.tcx();
114        let hir_id = tcx.local_def_id_to_hir_id(def_id);
115        let body_span = tcx.hir_span_with_body(hir_id);
116        dbg::solution!(genv, &answer, body_span);
117
118        let errors = answer.errors;
119        report_fixpoint_errors(genv, def_id, errors)
120    }
121}
122
123pub fn check_static(
124    genv: GlobalEnv,
125    cache: &mut FixQueryCache,
126    def_id: LocalDefId,
127    ty: rty::Ty,
128) -> Result<(), ErrorGuaranteed> {
129    // Build a PolyFnSig with no inputs and `ty` as the output
130    let output = rty::Binder::dummy(rty::FnOutput::new(ty, vec![]));
131    let fn_sig = rty::FnSig::new(
132        rustc_hir::Safety::Safe,
133        rustc_abi::ExternAbi::Rust,
134        rty::List::empty(),
135        rty::List::empty(),
136        output,
137        rty::Expr::ff(),
138        false,
139    );
140    let poly_sig = rty::PolyFnSig::dummy(fn_sig);
141
142    metrics::incr_metric(Metric::FnChecked, 1);
143    metrics::time_it(TimingKind::CheckBody(def_id), || check_body(genv, cache, def_id, &poly_sig))
144}
145
146pub fn check_fn(
147    genv: GlobalEnv,
148    cache: &mut FixQueryCache,
149    def_id: LocalDefId,
150) -> Result<(), ErrorGuaranteed> {
151    let span = genv.tcx().def_span(def_id);
152
153    // HACK(nilehmann) this will ignore any code generated by a macro. This is a temporary
154    // workaround to deal with a `#[derive(..)]` that generates code that flux cannot handle.
155    // Note that this is required because code generated by a `#[derive(..)]` cannot be
156    // manually trusted or ignored.
157    if !genv.tcx().def_span(def_id).ctxt().is_root() {
158        metrics::incr_metric(Metric::FnTrusted, 1);
159        return Ok(());
160    }
161
162    let opts = genv.infer_opts(def_id);
163
164    // FIXME(nilehmann) we should move this check to `compare_impl_item`
165    if let Some(infcx_root) = trait_impl_subtyping(genv, def_id, opts, span)
166        .with_span(span)
167        .map_err(|err| err.emit(genv, def_id))?
168    {
169        tracing::info!("check_fn::refine-subtyping");
170        let answer = infcx_root
171            .execute_fixpoint_query(cache, MaybeExternId::Local(def_id), FixpointQueryKind::Impl)
172            .emit(&genv)?;
173        tracing::info!("check_fn::fixpoint-subtyping");
174        let errors = answer.errors;
175        report_fixpoint_errors(genv, def_id, errors)?;
176    }
177
178    // Skip trusted functions
179    if genv.trusted(def_id) {
180        metrics::incr_metric(Metric::FnTrusted, 1);
181        return Ok(());
182    }
183
184    metrics::incr_metric(Metric::FnChecked, 1);
185    metrics::time_it(TimingKind::CheckBody(def_id), || -> Result<(), ErrorGuaranteed> {
186        let poly_sig = genv
187            .fn_sig(def_id)
188            .with_span(span)
189            .map_err(|err| err.emit(genv, def_id))?
190            .instantiate_identity();
191        let poly_sig = rty::auto_strong(genv, def_id, poly_sig);
192
193        check_body(genv, cache, def_id, &poly_sig)
194    })?;
195
196    dbg::check_fn_span!(genv.tcx(), def_id).in_scope(|| Ok(()))
197}
198
199fn report_errors(
200    genv: GlobalEnv,
201    local_id: LocalDefId,
202    errors: Vec<(Tag, TagIdx)>,
203) -> Result<(), ErrorGuaranteed> {
204    let log_path = if config::dump_constraint() {
205        let path = dbg::item_dump_path(genv.tcx(), local_id.to_def_id(), "smt2");
206        if path.exists() { Some(path) } else { None }
207    } else {
208        None
209    };
210
211    let mut e = None;
212    for (err, tag_idx) in errors {
213        let span = err.src_span;
214        let emit = |mut diag: rustc_errors::Diag<'_, ErrorGuaranteed>| -> ErrorGuaranteed {
215            if let Some(path) = &log_path {
216                diag.arg("path", path.display().to_string());
217                diag.arg("tag", tag_idx.to_string());
218                diag.note(crate::fluent_generated::refineck_constraint_log_note);
219            }
220            diag.emit()
221        };
222        let dcx = genv.sess().dcx().handle();
223        e = Some(match err.reason {
224            ConstrReason::Call
225            | ConstrReason::Subtype(SubtypeReason::Input)
226            | ConstrReason::Subtype(SubtypeReason::Requires)
227            | ConstrReason::Predicate => {
228                emit(
229                    errors::RefineError::call(span, err.dst_span)
230                        .into_diag(dcx, rustc_errors::Level::Error),
231                )
232            }
233            ConstrReason::Assign => {
234                emit(errors::AssignError { span }.into_diag(dcx, rustc_errors::Level::Error))
235            }
236            ConstrReason::Ret
237            | ConstrReason::Subtype(SubtypeReason::Output)
238            | ConstrReason::Subtype(SubtypeReason::Ensures) => {
239                emit(
240                    errors::RefineError::ret(span, err.dst_span)
241                        .into_diag(dcx, rustc_errors::Level::Error),
242                )
243            }
244            ConstrReason::Div => {
245                emit(errors::DivError { span }.into_diag(dcx, rustc_errors::Level::Error))
246            }
247            ConstrReason::Rem => {
248                emit(errors::RemError { span }.into_diag(dcx, rustc_errors::Level::Error))
249            }
250            ConstrReason::Goto(_) => {
251                emit(errors::GotoError { span }.into_diag(dcx, rustc_errors::Level::Error))
252            }
253            ConstrReason::Assert(msg) => {
254                emit(errors::AssertError { span, msg }.into_diag(dcx, rustc_errors::Level::Error))
255            }
256            ConstrReason::Fold | ConstrReason::FoldLocal => {
257                emit(
258                    errors::FoldError::new(span, err.dst_span)
259                        .into_diag(dcx, rustc_errors::Level::Error),
260                )
261            }
262            ConstrReason::Overflow => {
263                emit(errors::OverflowError { span }.into_diag(dcx, rustc_errors::Level::Error))
264            }
265            ConstrReason::Underflow => {
266                emit(errors::UnderflowError { span }.into_diag(dcx, rustc_errors::Level::Error))
267            }
268            ConstrReason::Other => {
269                emit(errors::UnknownError { span }.into_diag(dcx, rustc_errors::Level::Error))
270            }
271            ConstrReason::NoPanic(callee, reason) => {
272                emit(
273                    errors::PanicError {
274                        span,
275                        callee: genv.tcx().def_path_debug_str(callee),
276                        reason: format!("{:?}", reason),
277                    }
278                    .into_diag(dcx, rustc_errors::Level::Error),
279                )
280            }
281        });
282    }
283
284    if let Some(e) = e { Err(e) } else { Ok(()) }
285}
286
287fn report_expected_neg(genv: GlobalEnv, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
288    Err(genv.sess().emit_err(errors::ExpectedNeg {
289        span: genv.tcx().def_span(def_id),
290        def_descr: genv.tcx().def_descr(def_id.to_def_id()),
291    }))
292}
293
294mod errors {
295    use flux_errors::E0999;
296    use flux_macros::{Diagnostic, Subdiagnostic};
297    use flux_middle::rty::ESpan;
298    use rustc_span::Span;
299
300    #[derive(Diagnostic)]
301    #[diag(refineck_goto_error, code = E0999)]
302    pub struct GotoError {
303        #[primary_span]
304        pub span: Span,
305    }
306
307    #[derive(Diagnostic)]
308    #[diag(refineck_assign_error, code = E0999)]
309    pub struct AssignError {
310        #[primary_span]
311        pub span: Span,
312    }
313
314    #[derive(Subdiagnostic)]
315    #[note(refineck_condition_span_note)]
316    pub(crate) struct ConditionSpanNote {
317        #[primary_span]
318        pub span: Span,
319    }
320
321    #[derive(Subdiagnostic)]
322    #[note(refineck_call_span_note)]
323    pub(crate) struct CallSpanNote {
324        #[primary_span]
325        pub span: Span,
326    }
327
328    #[derive(Diagnostic)]
329    #[diag(refineck_refine_error, code = E0999)]
330    pub struct RefineError {
331        #[primary_span]
332        #[label]
333        pub span: Span,
334        cond: &'static str,
335        #[subdiagnostic]
336        span_note: Option<ConditionSpanNote>,
337        #[subdiagnostic]
338        call_span_note: Option<CallSpanNote>,
339    }
340
341    impl RefineError {
342        pub fn call(span: Span, espan: Option<ESpan>) -> Self {
343            RefineError::new("precondition", span, espan)
344        }
345
346        pub fn ret(span: Span, espan: Option<ESpan>) -> Self {
347            RefineError::new("postcondition", span, espan)
348        }
349
350        fn new(cond: &'static str, span: Span, espan: Option<ESpan>) -> RefineError {
351            match espan {
352                Some(dst_span) => {
353                    let span_note = Some(ConditionSpanNote { span: dst_span.span });
354                    let call_span_note = dst_span.base.map(|span| CallSpanNote { span });
355                    RefineError { span, cond, span_note, call_span_note }
356                }
357                None => RefineError { span, cond, span_note: None, call_span_note: None },
358            }
359        }
360    }
361
362    #[derive(Diagnostic)]
363    #[diag(refineck_div_error, code = E0999)]
364    pub struct DivError {
365        #[primary_span]
366        pub span: Span,
367    }
368
369    #[derive(Diagnostic)]
370    #[diag(refineck_rem_error, code = E0999)]
371    pub struct RemError {
372        #[primary_span]
373        pub span: Span,
374    }
375
376    #[derive(Diagnostic)]
377    #[diag(refineck_assert_error, code = E0999)]
378    pub struct AssertError {
379        #[primary_span]
380        pub span: Span,
381        pub msg: &'static str,
382    }
383
384    #[derive(Diagnostic)]
385    #[diag(refineck_fold_error, code = E0999)]
386    pub struct FoldError {
387        #[primary_span]
388        pub span: Span,
389        #[subdiagnostic]
390        span_note: Option<ConditionSpanNote>,
391    }
392
393    impl FoldError {
394        pub fn new(span: Span, espan: Option<ESpan>) -> Self {
395            let span_note = espan.map(|espan| ConditionSpanNote { span: espan.span });
396            FoldError { span, span_note }
397        }
398    }
399
400    #[derive(Diagnostic)]
401    #[diag(refineck_overflow_error, code = E0999)]
402    pub struct OverflowError {
403        #[primary_span]
404        pub span: Span,
405    }
406
407    #[derive(Diagnostic)]
408    #[diag(refineck_underflow_error, code = E0999)]
409    pub struct UnderflowError {
410        #[primary_span]
411        pub span: Span,
412    }
413
414    #[derive(Diagnostic)]
415    #[diag(refineck_unknown_error, code = E0999)]
416    pub struct UnknownError {
417        #[primary_span]
418        pub span: Span,
419    }
420
421    #[derive(Diagnostic)]
422    #[diag(refineck_expected_neg, code = E0999)]
423    pub struct ExpectedNeg {
424        #[primary_span]
425        pub span: Span,
426        pub def_descr: &'static str,
427    }
428
429    #[derive(Diagnostic)]
430    #[diag(refineck_panic_error, code = E0999)]
431    pub(super) struct PanicError {
432        #[primary_span]
433        pub(super) span: Span,
434        pub(super) callee: String,
435        pub(super) reason: String,
436    }
437}
flux_refineck/lib.rs

flux_refineck/
lib.rs
