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},
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, ESpan},
46};
47use rustc_data_structures::unord::UnordMap;
48use rustc_errors::ErrorGuaranteed;
49use rustc_hir::def_id::LocalDefId;
50use rustc_span::Span;
51
52use crate::{checker::errors::ResultExt as _, ghost_statements::compute_ghost_statements};
53
54fluent_messages! { "../locales/en-US.ftl" }
55
56fn report_fixpoint_errors(
57    genv: GlobalEnv,
58    local_id: LocalDefId,
59    errors: Vec<Tag>,
60) -> Result<(), ErrorGuaranteed> {
61    #[expect(clippy::collapsible_else_if, reason = "it looks better")]
62    if genv.should_fail(local_id) {
63        if errors.is_empty() { report_expected_neg(genv, local_id) } else { Ok(()) }
64    } else {
65        if errors.is_empty() { Ok(()) } else { report_errors(genv, errors) }
66    }
67}
68
69pub fn check_fn(
70    genv: GlobalEnv,
71    cache: &mut FixQueryCache,
72    def_id: LocalDefId,
73) -> Result<(), ErrorGuaranteed> {
74    let span = genv.tcx().def_span(def_id);
75
76    // HACK(nilehmann) this will ignore any code generated by a macro. This is a temporary
77    // workaround to deal with a `#[derive(..)]` that generates code that flux cannot handle.
78    // Note that this is required because code generated by a `#[derive(..)]` cannot be
79    // manually trusted or ignored.
80    if !genv.tcx().def_span(def_id).ctxt().is_root() {
81        metrics::incr_metric(Metric::FnTrusted, 1);
82        return Ok(());
83    }
84
85    let opts = genv.infer_opts(def_id);
86
87    // FIXME(nilehmann) we should move this check to `compare_impl_item`
88    if let Some(infcx_root) = trait_impl_subtyping(genv, def_id, opts, span)
89        .with_span(span)
90        .map_err(|err| err.emit(genv, def_id))?
91    {
92        tracing::info!("check_fn::refine-subtyping");
93        let answer = infcx_root
94            .execute_fixpoint_query(cache, MaybeExternId::Local(def_id), FixpointQueryKind::Impl)
95            .emit(&genv)?;
96        tracing::info!("check_fn::fixpoint-subtyping");
97        let errors = answer.errors;
98        report_fixpoint_errors(genv, def_id, errors)?;
99    }
100
101    // Skip trusted functions
102    if genv.trusted(def_id) {
103        metrics::incr_metric(Metric::FnTrusted, 1);
104        return Ok(());
105    }
106
107    metrics::incr_metric(Metric::FnChecked, 1);
108    metrics::time_it(TimingKind::CheckFn(def_id), || -> Result<(), ErrorGuaranteed> {
109        let ghost_stmts = compute_ghost_statements(genv, def_id)
110            .with_span(span)
111            .map_err(|err| err.emit(genv, def_id))?;
112        let mut closures = UnordMap::default();
113
114        let poly_sig = genv
115            .fn_sig(def_id)
116            .with_span(span)
117            .map_err(|err| err.emit(genv, def_id))?
118            .instantiate_identity();
119        let poly_sig = rty::auto_strong(genv, def_id, poly_sig);
120
121        // PHASE 1: infer shape of `TypeEnv` at the entry of join points
122        let shape_result =
123            Checker::run_in_shape_mode(genv, def_id, &ghost_stmts, &mut closures, opts, &poly_sig)
124                .map_err(|err| err.emit(genv, def_id))?;
125
126        // PHASE 2: generate refinement tree constraint
127        let infcx_root = Checker::run_in_refine_mode(
128            genv,
129            def_id,
130            &ghost_stmts,
131            &mut closures,
132            shape_result,
133            opts,
134            &poly_sig,
135        )
136        .map_err(|err| err.emit(genv, def_id))?;
137
138        if genv.proven_externally(def_id).is_some() {
139            if flux_config::lean().is_emit() {
140                infcx_root
141                    .execute_lean_query(MaybeExternId::Local(def_id))
142                    .emit(&genv)
143            } else {
144                Err(genv
145                    .sess()
146                    .emit_err(errors::MissingLean { span: genv.tcx().def_span(def_id) }))
147            }
148        } else {
149            // PHASE 3: invoke fixpoint on the constraint
150            let answer = infcx_root
151                .execute_fixpoint_query(
152                    cache,
153                    MaybeExternId::Local(def_id),
154                    FixpointQueryKind::Body,
155                )
156                .emit(&genv)?;
157
158            // DUMP SOLUTION
159            let tcx = genv.tcx();
160            let hir_id = tcx.local_def_id_to_hir_id(def_id);
161            let body_span = tcx.hir_span_with_body(hir_id);
162            dbg::solution!(genv, &answer.solution, body_span);
163
164            let errors = answer.errors;
165            report_fixpoint_errors(genv, def_id, errors)
166        }
167    })?;
168
169    dbg::check_fn_span!(genv.tcx(), def_id).in_scope(|| Ok(()))
170}
171
172fn call_error(genv: GlobalEnv, span: Span, dst_span: Option<ESpan>) -> ErrorGuaranteed {
173    genv.sess()
174        .emit_err(errors::RefineError::call(span, dst_span))
175}
176
177fn ret_error(genv: GlobalEnv, span: Span, dst_span: Option<ESpan>) -> ErrorGuaranteed {
178    genv.sess()
179        .emit_err(errors::RefineError::ret(span, dst_span))
180}
181
182fn report_errors(genv: GlobalEnv, errors: Vec<Tag>) -> Result<(), ErrorGuaranteed> {
183    let mut e = None;
184    for err in errors {
185        let span = err.src_span;
186        e = Some(match err.reason {
187            ConstrReason::Call
188            | ConstrReason::Subtype(SubtypeReason::Input)
189            | ConstrReason::Subtype(SubtypeReason::Requires)
190            | ConstrReason::Predicate => call_error(genv, span, err.dst_span),
191            ConstrReason::Assign => genv.sess().emit_err(errors::AssignError { span }),
192            ConstrReason::Ret
193            | ConstrReason::Subtype(SubtypeReason::Output)
194            | ConstrReason::Subtype(SubtypeReason::Ensures) => ret_error(genv, span, err.dst_span),
195            ConstrReason::Div => genv.sess().emit_err(errors::DivError { span }),
196            ConstrReason::Rem => genv.sess().emit_err(errors::RemError { span }),
197            ConstrReason::Goto(_) => genv.sess().emit_err(errors::GotoError { span }),
198            ConstrReason::Assert(msg) => genv.sess().emit_err(errors::AssertError { span, msg }),
199            ConstrReason::Fold | ConstrReason::FoldLocal => {
200                genv.sess().emit_err(errors::FoldError { span })
201            }
202            ConstrReason::Overflow => genv.sess().emit_err(errors::OverflowError { span }),
203            ConstrReason::Underflow => genv.sess().emit_err(errors::UnderflowError { span }),
204            ConstrReason::Other => genv.sess().emit_err(errors::UnknownError { span }),
205        });
206    }
207
208    if let Some(e) = e { Err(e) } else { Ok(()) }
209}
210
211fn report_expected_neg(genv: GlobalEnv, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
212    Err(genv.sess().emit_err(errors::ExpectedNeg {
213        span: genv.tcx().def_span(def_id),
214        def_descr: genv.tcx().def_descr(def_id.to_def_id()),
215    }))
216}
217
218mod errors {
219    use flux_errors::E0999;
220    use flux_macros::{Diagnostic, Subdiagnostic};
221    use flux_middle::rty::ESpan;
222    use rustc_span::Span;
223
224    #[derive(Diagnostic)]
225    #[diag(refineck_goto_error, code = E0999)]
226    pub struct GotoError {
227        #[primary_span]
228        pub span: Span,
229    }
230
231    #[derive(Diagnostic)]
232    #[diag(refineck_assign_error, code = E0999)]
233    pub struct AssignError {
234        #[primary_span]
235        pub span: Span,
236    }
237
238    #[derive(Subdiagnostic)]
239    #[note(refineck_condition_span_note)]
240    pub(crate) struct ConditionSpanNote {
241        #[primary_span]
242        pub span: Span,
243    }
244
245    #[derive(Subdiagnostic)]
246    #[note(refineck_call_span_note)]
247    pub(crate) struct CallSpanNote {
248        #[primary_span]
249        pub span: Span,
250    }
251
252    #[derive(Diagnostic)]
253    #[diag(refineck_refine_error, code = E0999)]
254    pub struct RefineError {
255        #[primary_span]
256        #[label]
257        pub span: Span,
258        cond: &'static str,
259        #[subdiagnostic]
260        span_note: Option<ConditionSpanNote>,
261        #[subdiagnostic]
262        call_span_note: Option<CallSpanNote>,
263    }
264
265    impl RefineError {
266        pub fn call(span: Span, espan: Option<ESpan>) -> Self {
267            RefineError::new("precondition", span, espan)
268        }
269
270        pub fn ret(span: Span, espan: Option<ESpan>) -> Self {
271            RefineError::new("postcondition", span, espan)
272        }
273
274        fn new(cond: &'static str, span: Span, espan: Option<ESpan>) -> RefineError {
275            match espan {
276                Some(dst_span) => {
277                    let span_note = Some(ConditionSpanNote { span: dst_span.span });
278                    let call_span_note = dst_span.base.map(|span| CallSpanNote { span });
279                    RefineError { span, cond, span_note, call_span_note }
280                }
281                None => RefineError { span, cond, span_note: None, call_span_note: None },
282            }
283        }
284    }
285
286    #[derive(Diagnostic)]
287    #[diag(refineck_div_error, code = E0999)]
288    pub struct DivError {
289        #[primary_span]
290        pub span: Span,
291    }
292
293    #[derive(Diagnostic)]
294    #[diag(refineck_rem_error, code = E0999)]
295    pub struct RemError {
296        #[primary_span]
297        pub span: Span,
298    }
299
300    #[derive(Diagnostic)]
301    #[diag(refineck_assert_error, code = E0999)]
302    pub struct AssertError {
303        #[primary_span]
304        pub span: Span,
305        pub msg: &'static str,
306    }
307
308    #[derive(Diagnostic)]
309    #[diag(refineck_fold_error, code = E0999)]
310    pub struct FoldError {
311        #[primary_span]
312        pub span: Span,
313    }
314
315    #[derive(Diagnostic)]
316    #[diag(refineck_overflow_error, code = E0999)]
317    pub struct OverflowError {
318        #[primary_span]
319        pub span: Span,
320    }
321
322    #[derive(Diagnostic)]
323    #[diag(refineck_underflow_error, code = E0999)]
324    pub struct UnderflowError {
325        #[primary_span]
326        pub span: Span,
327    }
328
329    #[derive(Diagnostic)]
330    #[diag(refineck_unknown_error, code = E0999)]
331    pub struct UnknownError {
332        #[primary_span]
333        pub span: Span,
334    }
335
336    #[derive(Diagnostic)]
337    #[diag(refineck_expected_neg, code = E0999)]
338    pub struct ExpectedNeg {
339        #[primary_span]
340        pub span: Span,
341        pub def_descr: &'static str,
342    }
343
344    #[derive(Diagnostic)]
345    #[diag(refineck_missing_lean, code = E0999)]
346    pub struct MissingLean {
347        #[primary_span]
348        pub span: Span,
349    }
350}
flux_refineck/lib.rs

flux_refineck/
lib.rs
