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

flux_refineck/
lib.rs
