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

flux_refineck/
lib.rs
