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        // PHASE 1: infer shape of `TypeEnv` at the entry of join points
114        let shape_result =
115            Checker::run_in_shape_mode(genv, def_id, &ghost_stmts, &mut closures, opts)
116                .map_err(|err| err.emit(genv, def_id))?;
117
118        // PHASE 2: generate refinement tree constraint
119        let infcx_root = Checker::run_in_refine_mode(
120            genv,
121            def_id,
122            &ghost_stmts,
123            &mut closures,
124            shape_result,
125            opts,
126        )
127        .map_err(|err| err.emit(genv, def_id))?;
128
129        if genv.proven_externally(def_id) {
130            if flux_config::emit_lean_defs() {
131                infcx_root
132                    .execute_lean_query(MaybeExternId::Local(def_id))
133                    .emit(&genv)
134            } else {
135                panic!("emit_lean_defs should be enabled if there are externally proven items");
136            }
137        } else {
138            // PHASE 3: invoke fixpoint on the constraint
139            let answer = infcx_root
140                .execute_fixpoint_query(
141                    cache,
142                    MaybeExternId::Local(def_id),
143                    FixpointQueryKind::Body,
144                )
145                .emit(&genv)?;
146
147            // DUMP SOLUTION
148            let tcx = genv.tcx();
149            let hir_id = tcx.local_def_id_to_hir_id(def_id);
150            let body_span = tcx.hir_span_with_body(hir_id);
151            dbg::solution!(genv, &answer.solution, body_span);
152
153            let errors = answer.errors;
154            report_fixpoint_errors(genv, def_id, errors)
155        }
156    })?;
157
158    dbg::check_fn_span!(genv.tcx(), def_id).in_scope(|| Ok(()))
159}
160
161fn call_error(genv: GlobalEnv, span: Span, dst_span: Option<ESpan>) -> ErrorGuaranteed {
162    genv.sess()
163        .emit_err(errors::RefineError::call(span, dst_span))
164}
165
166fn ret_error(genv: GlobalEnv, span: Span, dst_span: Option<ESpan>) -> ErrorGuaranteed {
167    genv.sess()
168        .emit_err(errors::RefineError::ret(span, dst_span))
169}
170
171fn report_errors(genv: GlobalEnv, errors: Vec<Tag>) -> Result<(), ErrorGuaranteed> {
172    let mut e = None;
173    for err in errors {
174        let span = err.src_span;
175        e = Some(match err.reason {
176            ConstrReason::Call
177            | ConstrReason::Subtype(SubtypeReason::Input)
178            | ConstrReason::Subtype(SubtypeReason::Requires)
179            | ConstrReason::Predicate => call_error(genv, span, err.dst_span),
180            ConstrReason::Assign => genv.sess().emit_err(errors::AssignError { span }),
181            ConstrReason::Ret
182            | ConstrReason::Subtype(SubtypeReason::Output)
183            | ConstrReason::Subtype(SubtypeReason::Ensures) => ret_error(genv, span, err.dst_span),
184            ConstrReason::Div => genv.sess().emit_err(errors::DivError { span }),
185            ConstrReason::Rem => genv.sess().emit_err(errors::RemError { span }),
186            ConstrReason::Goto(_) => genv.sess().emit_err(errors::GotoError { span }),
187            ConstrReason::Assert(msg) => genv.sess().emit_err(errors::AssertError { span, msg }),
188            ConstrReason::Fold | ConstrReason::FoldLocal => {
189                genv.sess().emit_err(errors::FoldError { span })
190            }
191            ConstrReason::Overflow => genv.sess().emit_err(errors::OverflowError { span }),
192            ConstrReason::Underflow => genv.sess().emit_err(errors::UnderflowError { span }),
193            ConstrReason::Other => genv.sess().emit_err(errors::UnknownError { span }),
194        });
195    }
196
197    if let Some(e) = e { Err(e) } else { Ok(()) }
198}
199
200fn report_expected_neg(genv: GlobalEnv, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
201    Err(genv.sess().emit_err(errors::ExpectedNeg {
202        span: genv.tcx().def_span(def_id),
203        def_descr: genv.tcx().def_descr(def_id.to_def_id()),
204    }))
205}
206
207mod errors {
208    use flux_errors::E0999;
209    use flux_macros::{Diagnostic, Subdiagnostic};
210    use flux_middle::rty::ESpan;
211    use rustc_span::Span;
212
213    #[derive(Diagnostic)]
214    #[diag(refineck_goto_error, code = E0999)]
215    pub struct GotoError {
216        #[primary_span]
217        pub span: Span,
218    }
219
220    #[derive(Diagnostic)]
221    #[diag(refineck_assign_error, code = E0999)]
222    pub struct AssignError {
223        #[primary_span]
224        pub span: Span,
225    }
226
227    #[derive(Subdiagnostic)]
228    #[note(refineck_condition_span_note)]
229    pub(crate) struct ConditionSpanNote {
230        #[primary_span]
231        pub span: Span,
232    }
233
234    #[derive(Subdiagnostic)]
235    #[note(refineck_call_span_note)]
236    pub(crate) struct CallSpanNote {
237        #[primary_span]
238        pub span: Span,
239    }
240
241    #[derive(Diagnostic)]
242    #[diag(refineck_refine_error, code = E0999)]
243    pub struct RefineError {
244        #[primary_span]
245        #[label]
246        pub span: Span,
247        cond: &'static str,
248        #[subdiagnostic]
249        span_note: Option<ConditionSpanNote>,
250        #[subdiagnostic]
251        call_span_note: Option<CallSpanNote>,
252    }
253
254    impl RefineError {
255        pub fn call(span: Span, espan: Option<ESpan>) -> Self {
256            RefineError::new("precondition", span, espan)
257        }
258
259        pub fn ret(span: Span, espan: Option<ESpan>) -> Self {
260            RefineError::new("postcondition", span, espan)
261        }
262
263        fn new(cond: &'static str, span: Span, espan: Option<ESpan>) -> RefineError {
264            match espan {
265                Some(dst_span) => {
266                    let span_note = Some(ConditionSpanNote { span: dst_span.span });
267                    let call_span_note = dst_span.base.map(|span| CallSpanNote { span });
268                    RefineError { span, cond, span_note, call_span_note }
269                }
270                None => RefineError { span, cond, span_note: None, call_span_note: None },
271            }
272        }
273    }
274
275    #[derive(Diagnostic)]
276    #[diag(refineck_div_error, code = E0999)]
277    pub struct DivError {
278        #[primary_span]
279        pub span: Span,
280    }
281
282    #[derive(Diagnostic)]
283    #[diag(refineck_rem_error, code = E0999)]
284    pub struct RemError {
285        #[primary_span]
286        pub span: Span,
287    }
288
289    #[derive(Diagnostic)]
290    #[diag(refineck_assert_error, code = E0999)]
291    pub struct AssertError {
292        #[primary_span]
293        pub span: Span,
294        pub msg: &'static str,
295    }
296
297    #[derive(Diagnostic)]
298    #[diag(refineck_fold_error, code = E0999)]
299    pub struct FoldError {
300        #[primary_span]
301        pub span: Span,
302    }
303
304    #[derive(Diagnostic)]
305    #[diag(refineck_overflow_error, code = E0999)]
306    pub struct OverflowError {
307        #[primary_span]
308        pub span: Span,
309    }
310
311    #[derive(Diagnostic)]
312    #[diag(refineck_underflow_error, code = E0999)]
313    pub struct UnderflowError {
314        #[primary_span]
315        pub span: Span,
316    }
317
318    #[derive(Diagnostic)]
319    #[diag(refineck_unknown_error, code = E0999)]
320    pub struct UnknownError {
321        #[primary_span]
322        pub span: Span,
323    }
324
325    #[derive(Diagnostic)]
326    #[diag(refineck_expected_neg, code = E0999)]
327    pub struct ExpectedNeg {
328        #[primary_span]
329        pub span: Span,
330        pub def_descr: &'static str,
331    }
332}
flux_refineck/lib.rs

flux_refineck/
lib.rs
