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

flux_refineck/
lib.rs
