flux_refineck/
lib.rs

Help
1//! Refinement type checking
2
3#![feature(
4    associated_type_defaults,
5    box_patterns,
6    if_let_guard,
7    let_chains,
8    min_specialization,
9    never_type,
10    rustc_private,
11    unwrap_infallible
12)]
13
14extern crate rustc_abi;
15extern crate rustc_data_structures;
16extern crate rustc_errors;
17extern crate rustc_hir;
18extern crate rustc_index;
19extern crate rustc_infer;
20extern crate rustc_middle;
21extern crate rustc_mir_dataflow;
22extern crate rustc_span;
23extern crate rustc_type_ir;
24
25mod checker;
26pub mod compare_impl_item;
27mod ghost_statements;
28pub mod invariants;
29mod primops;
30mod queue;
31mod type_env;
32
33use checker::{Checker, trait_impl_subtyping};
34use flux_common::{dbg, result::ResultExt as _};
35use flux_infer::{
36    fixpoint_encoding::FixQueryCache,
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    rty::{self, ESpan},
45    timings,
46};
47use itertools::Itertools;
48use rustc_data_structures::unord::UnordMap;
49use rustc_errors::ErrorGuaranteed;
50use rustc_hir::def_id::LocalDefId;
51use rustc_span::Span;
52
53use crate::{checker::errors::ResultExt as _, ghost_statements::compute_ghost_statements};
54
55fluent_messages! { "../locales/en-US.ftl" }
56
57fn report_fixpoint_errors(
58    genv: GlobalEnv,
59    local_id: LocalDefId,
60    errors: Vec<Tag>,
61) -> Result<(), ErrorGuaranteed> {
62    #[expect(clippy::collapsible_else_if, reason = "it looks better")]
63    if genv.should_fail(local_id) {
64        if errors.is_empty() { report_expected_neg(genv, local_id) } else { Ok(()) }
65    } else {
66        if errors.is_empty() { Ok(()) } else { report_errors(genv, errors) }
67    }
68}
69
70pub fn check_fn(
71    genv: GlobalEnv,
72    cache: &mut FixQueryCache,
73    def_id: LocalDefId,
74) -> Result<(), ErrorGuaranteed> {
75    let span = genv.tcx().def_span(def_id);
76
77    // HACK(nilehmann) this will ignore any code generated by a macro. This is a temporary
78    // workaround to deal with a `#[derive(..)]` that generates code that flux cannot handle.
79    // Note that this is required because code generated by a `#[derive(..)]` cannot be
80    // manually trusted or ignored.
81    if !genv.tcx().def_span(def_id).ctxt().is_root() {
82        return Ok(());
83    }
84
85    // Skip trait methods without body
86    if genv.tcx().hir_node_by_def_id(def_id).body_id().is_none() {
87        return Ok(());
88    }
89
90    let opts = genv.infer_opts(def_id);
91
92    // FIXME(nilehmann) we should move this check to `compare_impl_item`
93    if let Some(infcx_root) = trait_impl_subtyping(genv, def_id, opts, span)
94        .with_span(span)
95        .map_err(|err| err.emit(genv, def_id))?
96    {
97        tracing::info!("check_fn::refine-subtyping");
98        let errors = infcx_root
99            .execute_fixpoint_query(cache, MaybeExternId::Local(def_id), FixpointQueryKind::Impl)
100            .emit(&genv)?;
101        tracing::info!("check_fn::fixpoint-subtyping");
102        report_fixpoint_errors(genv, def_id, errors)?;
103    }
104
105    // Skip trusted functions
106    if genv.trusted(def_id) {
107        return Ok(());
108    }
109
110    timings::time_it(timings::TimingKind::CheckFn(def_id), || -> Result<(), ErrorGuaranteed> {
111        let ghost_stmts = compute_ghost_statements(genv, def_id)
112            .with_span(span)
113            .map_err(|err| err.emit(genv, def_id))?;
114        let mut closures = UnordMap::default();
115        // PHASE 1: infer shape of `TypeEnv` at the entry of join points
116        let shape_result =
117            Checker::run_in_shape_mode(genv, def_id, &ghost_stmts, &mut closures, opts)
118                .map_err(|err| err.emit(genv, def_id))?;
119
120        // PHASE 2: generate refinement tree constraint
121        let infcx_root = Checker::run_in_refine_mode(
122            genv,
123            def_id,
124            &ghost_stmts,
125            &mut closures,
126            shape_result,
127            opts,
128        )
129        .map_err(|err| err.emit(genv, def_id))?;
130
131        // PHASE 3: invoke fixpoint on the constraint
132        let errors = infcx_root
133            .execute_fixpoint_query(cache, MaybeExternId::Local(def_id), FixpointQueryKind::Body)
134            .emit(&genv)?;
135        report_fixpoint_errors(genv, def_id, errors)
136    })?;
137
138    dbg::check_fn_span!(genv.tcx(), def_id).in_scope(|| Ok(()))
139}
140
141fn call_error(genv: GlobalEnv, span: Span, dst_span: Option<ESpan>) -> ErrorGuaranteed {
142    genv.sess()
143        .emit_err(errors::RefineError::call(span, dst_span))
144}
145
146fn ret_error(genv: GlobalEnv, span: Span, dst_span: Option<ESpan>) -> ErrorGuaranteed {
147    genv.sess()
148        .emit_err(errors::RefineError::ret(span, dst_span))
149}
150
151fn report_errors(genv: GlobalEnv, errors: Vec<Tag>) -> Result<(), ErrorGuaranteed> {
152    let mut e = None;
153    for err in errors {
154        let span = err.src_span;
155        e = Some(match err.reason {
156            ConstrReason::Call
157            | ConstrReason::Subtype(SubtypeReason::Input)
158            | ConstrReason::Subtype(SubtypeReason::Requires)
159            | ConstrReason::Predicate => call_error(genv, span, err.dst_span),
160            ConstrReason::Assign => genv.sess().emit_err(errors::AssignError { span }),
161            ConstrReason::Ret
162            | ConstrReason::Subtype(SubtypeReason::Output)
163            | ConstrReason::Subtype(SubtypeReason::Ensures) => ret_error(genv, span, err.dst_span),
164            ConstrReason::Div => genv.sess().emit_err(errors::DivError { span }),
165            ConstrReason::Rem => genv.sess().emit_err(errors::RemError { span }),
166            ConstrReason::Goto(_) => genv.sess().emit_err(errors::GotoError { span }),
167            ConstrReason::Assert(msg) => genv.sess().emit_err(errors::AssertError { span, msg }),
168            ConstrReason::Fold | ConstrReason::FoldLocal => {
169                genv.sess().emit_err(errors::FoldError { span })
170            }
171            ConstrReason::Overflow => genv.sess().emit_err(errors::OverflowError { span }),
172            ConstrReason::Other => genv.sess().emit_err(errors::UnknownError { span }),
173        });
174    }
175
176    if let Some(e) = e { Err(e) } else { Ok(()) }
177}
178
179fn report_expected_neg(genv: GlobalEnv, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
180    Err(genv.sess().emit_err(errors::ExpectedNeg {
181        span: genv.tcx().def_span(def_id),
182        def_descr: genv.tcx().def_descr(def_id.to_def_id()),
183    }))
184}
185
186mod errors {
187    use flux_errors::E0999;
188    use flux_macros::{Diagnostic, Subdiagnostic};
189    use flux_middle::rty::ESpan;
190    use rustc_span::Span;
191
192    #[derive(Diagnostic)]
193    #[diag(refineck_goto_error, code = E0999)]
194    pub struct GotoError {
195        #[primary_span]
196        pub span: Span,
197    }
198
199    #[derive(Diagnostic)]
200    #[diag(refineck_assign_error, code = E0999)]
201    pub struct AssignError {
202        #[primary_span]
203        pub span: Span,
204    }
205
206    #[derive(Subdiagnostic)]
207    #[note(refineck_condition_span_note)]
208    pub(crate) struct ConditionSpanNote {
209        #[primary_span]
210        pub span: Span,
211    }
212
213    #[derive(Subdiagnostic)]
214    #[note(refineck_call_span_note)]
215    pub(crate) struct CallSpanNote {
216        #[primary_span]
217        pub span: Span,
218    }
219
220    #[derive(Diagnostic)]
221    #[diag(refineck_refine_error, code = E0999)]
222    pub struct RefineError {
223        #[primary_span]
224        #[label]
225        pub span: Span,
226        cond: &'static str,
227        #[subdiagnostic]
228        span_note: Option<ConditionSpanNote>,
229        #[subdiagnostic]
230        call_span_note: Option<CallSpanNote>,
231    }
232
233    impl RefineError {
234        pub fn call(span: Span, espan: Option<ESpan>) -> Self {
235            RefineError::new("precondition", span, espan)
236        }
237
238        pub fn ret(span: Span, espan: Option<ESpan>) -> Self {
239            RefineError::new("postcondition", span, espan)
240        }
241
242        fn new(cond: &'static str, span: Span, espan: Option<ESpan>) -> RefineError {
243            match espan {
244                Some(dst_span) => {
245                    let span_note = Some(ConditionSpanNote { span: dst_span.span });
246                    let call_span_note = dst_span.base.map(|span| CallSpanNote { span });
247                    RefineError { span, cond, span_note, call_span_note }
248                }
249                None => RefineError { span, cond, span_note: None, call_span_note: None },
250            }
251        }
252    }
253
254    #[derive(Diagnostic)]
255    #[diag(refineck_div_error, code = E0999)]
256    pub struct DivError {
257        #[primary_span]
258        pub span: Span,
259    }
260
261    #[derive(Diagnostic)]
262    #[diag(refineck_rem_error, code = E0999)]
263    pub struct RemError {
264        #[primary_span]
265        pub span: Span,
266    }
267
268    #[derive(Diagnostic)]
269    #[diag(refineck_assert_error, code = E0999)]
270    pub struct AssertError {
271        #[primary_span]
272        pub span: Span,
273        pub msg: &'static str,
274    }
275
276    #[derive(Diagnostic)]
277    #[diag(refineck_fold_error, code = E0999)]
278    pub struct FoldError {
279        #[primary_span]
280        pub span: Span,
281    }
282
283    #[derive(Diagnostic)]
284    #[diag(refineck_overflow_error, code = E0999)]
285    pub struct OverflowError {
286        #[primary_span]
287        pub span: Span,
288    }
289
290    #[derive(Diagnostic)]
291    #[diag(refineck_unknown_error, code = E0999)]
292    pub struct UnknownError {
293        #[primary_span]
294        pub span: Span,
295    }
296
297    #[derive(Diagnostic)]
298    #[diag(refineck_expected_neg, code = E0999)]
299    pub struct ExpectedNeg {
300        #[primary_span]
301        pub span: Span,
302        pub def_descr: &'static str,
303    }
304}
flux_refineck/lib.rs

flux_refineck/
lib.rs
