1#![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 if !genv.tcx().def_span(def_id).ctxt().is_root() {
80 return Ok(());
81 }
82
83 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 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 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 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 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 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}