flux_driver/
callbacks.rs

1use std::{io, path::Path};
2
3use flux_common::{bug, cache::QueryCache, iter::IterExt, result::ResultExt};
4use flux_config::{self as config};
5use flux_errors::FluxSession;
6use flux_infer::{
7    fixpoint_encoding::{ExprEncodingCtxt, FixQueryCache, SortEncodingCtxt},
8    lean_encoding::LeanEncoder,
9};
10use flux_metadata::CStore;
11use flux_middle::{
12    Specs,
13    def_id::MaybeExternId,
14    fhir::{self, FluxItem},
15    global_env::GlobalEnv,
16    metrics::{self, Metric, TimingKind},
17    queries::{Providers, QueryResult},
18};
19use flux_refineck as refineck;
20use itertools::Itertools;
21use rustc_borrowck::consumers::ConsumerOptions;
22use rustc_driver::{Callbacks, Compilation};
23use rustc_errors::ErrorGuaranteed;
24use rustc_hir::{
25    def::DefKind,
26    def_id::{DefId, LOCAL_CRATE, LocalDefId},
27};
28use rustc_interface::interface::Compiler;
29use rustc_middle::{query, ty::TyCtxt};
30use rustc_session::config::OutputType;
31use rustc_span::FileName;
32
33use crate::{DEFAULT_LOCALE_RESOURCES, collector::SpecCollector};
34
35#[derive(Default)]
36pub struct FluxCallbacks;
37
38impl Callbacks for FluxCallbacks {
39    fn config(&mut self, config: &mut rustc_interface::interface::Config) {
40        assert!(config.override_queries.is_none());
41
42        config.override_queries = Some(|_, local| {
43            local.mir_borrowck = mir_borrowck;
44        });
45        // this should always be empty otherwise something changed in rustc and all our assumptions
46        // about symbol interning are wrong.
47        assert!(config.extra_symbols.is_empty());
48        config.extra_symbols = flux_syntax::symbols::PREDEFINED_FLUX_SYMBOLS.to_vec();
49    }
50
51    fn after_analysis(&mut self, compiler: &Compiler, tcx: TyCtxt<'_>) -> Compilation {
52        self.verify(compiler, tcx);
53        if config::full_compilation() { Compilation::Continue } else { Compilation::Stop }
54    }
55}
56
57impl FluxCallbacks {
58    fn verify(&self, compiler: &Compiler, tcx: TyCtxt<'_>) {
59        if compiler.sess.dcx().has_errors().is_some() {
60            return;
61        }
62
63        let sess = FluxSession::new(
64            &tcx.sess.opts,
65            tcx.sess.psess.clone_source_map(),
66            rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false),
67        );
68
69        let mut providers = Providers::default();
70        flux_desugar::provide(&mut providers);
71        flux_fhir_analysis::provide(&mut providers);
72        providers.collect_specs = collect_specs;
73
74        let cstore = CStore::load(tcx, &sess);
75        let arena = fhir::Arena::new();
76        GlobalEnv::enter(tcx, &sess, Box::new(cstore), &arena, providers, |genv| {
77            let result = metrics::time_it(TimingKind::Total, || check_crate(genv));
78            if result.is_ok() {
79                encode_and_save_metadata(genv);
80            }
81        });
82        let _ = metrics::print_and_dump_timings(tcx);
83        sess.finish_diagnostics();
84    }
85}
86
87fn check_crate(genv: GlobalEnv) -> Result<(), ErrorGuaranteed> {
88    tracing::info_span!("check_crate").in_scope(move || {
89        tracing::info!("Callbacks::check_wf");
90        // Query qualifiers and spec funcs to report wf errors
91        let _ = genv.qualifiers().emit(&genv)?;
92        let _ = genv.normalized_defns(LOCAL_CRATE);
93
94        let mut ck = CrateChecker::new(genv);
95        if config::emit_lean_defs() {
96            ck.encode_flux_items_in_lean().unwrap_or(());
97        }
98
99        let crate_items = genv.tcx().hir_crate_items(());
100
101        let dups = crate_items.definitions().duplicates().collect_vec();
102        if !dups.is_empty() {
103            bug!("TODO: {dups:#?}");
104        }
105        let result = crate_items
106            .definitions()
107            .try_for_each_exhaust(|def_id| ck.check_def_catching_bugs(def_id));
108
109        ck.cache.save().unwrap_or(());
110
111        tracing::info!("Callbacks::check_crate");
112
113        result
114    })
115}
116
117fn collect_specs(genv: GlobalEnv) -> Specs {
118    match SpecCollector::collect(genv.tcx(), genv.sess()) {
119        Ok(specs) => specs,
120        Err(err) => {
121            genv.sess().abort(err);
122        }
123    }
124}
125
126fn encode_and_save_metadata(genv: GlobalEnv) {
127    // HACK(nilehmann) do not encode metadata for `core`, this is so verify-rust-std works even
128    // if it has unsupported items. We report errors lazily so partially analyzing the crate should
129    // skip the error, except that encoding the metadata for the crate will trigger conversion for
130    // all items which can trigger the error even if not included for analysis. To fix this properly
131    // we should consider how to handle metadata encoding if only part of the crate is included for
132    // analysis.
133    if genv.tcx().crate_name(LOCAL_CRATE) == flux_syntax::symbols::sym::core {
134        return;
135    }
136
137    // We only save metadata when `--emit=metadata` is passed as an argument. In this case, we save
138    // the `.fluxmeta` file alongside the `.rmeta` file. This setup works for `cargo flux`, which
139    // wraps `cargo check` and always passes `--emit=metadata`. Tests also explicitly pass this flag.
140    let tcx = genv.tcx();
141    if tcx
142        .output_filenames(())
143        .outputs
144        .contains_key(&OutputType::Metadata)
145    {
146        let path = flux_metadata::filename_for_metadata(tcx);
147        flux_metadata::encode_metadata(genv, path.as_path());
148    }
149}
150
151struct CrateChecker<'genv, 'tcx> {
152    genv: GlobalEnv<'genv, 'tcx>,
153    cache: FixQueryCache,
154}
155
156impl<'genv, 'tcx> CrateChecker<'genv, 'tcx> {
157    fn new(genv: GlobalEnv<'genv, 'tcx>) -> Self {
158        Self { genv, cache: QueryCache::load() }
159    }
160
161    pub(crate) fn encode_flux_items_in_lean(&self) -> Result<(), io::Error> {
162        let mut ecx = ExprEncodingCtxt::new(self.genv, None);
163        let mut scx = SortEncodingCtxt::default();
164        let mut fun_defs = vec![];
165        let mut opaque_fun_defs = vec![];
166        for (def_id, flux_item) in self.genv.fhir_iter_flux_items() {
167            ecx.declare_fun(def_id.to_def_id());
168            match flux_item {
169                FluxItem::Func(spec_func) if spec_func.body.is_some() => {
170                    if spec_func.params == 0 {
171                        fun_defs.push(
172                            ecx.fun_def_to_fixpoint(spec_func.def_id.to_def_id(), &mut scx)
173                                .unwrap(),
174                        );
175                    }
176                }
177                FluxItem::Func(spec_func) => {
178                    opaque_fun_defs
179                        .push(ecx.fun_decl_to_fixpoint(spec_func.def_id.to_def_id(), &mut scx));
180                }
181                FluxItem::SortDecl(sort_decl) => {
182                    scx.declare_opaque_sort(sort_decl.def_id.to_def_id());
183                }
184                _ => {}
185            }
186        }
187        let opaque_sorts = scx.user_sorts_to_fixpoint(self.genv);
188        let adt_defs = scx.encode_data_decls(self.genv).unwrap();
189        if !opaque_sorts.is_empty()
190            || !opaque_fun_defs.is_empty()
191            || !adt_defs.is_empty()
192            || !fun_defs.is_empty()
193        {
194            let encoder = LeanEncoder::new(
195                self.genv,
196                std::path::Path::new("./"),
197                "lean_proofs".to_string(),
198                "Defs".to_string(),
199            );
200            encoder
201                .encode_defs(&opaque_sorts, &opaque_fun_defs, &adt_defs, &fun_defs)
202                .unwrap();
203        }
204        Ok(())
205    }
206
207    fn matches_def(&self, def_id: MaybeExternId, def: &str) -> bool {
208        // Does this def_id's name contain `fn_name`?
209        let def_path = self.genv.tcx().def_path_str(def_id.local_id());
210        def_path.contains(def)
211    }
212
213    fn matches_file_path<F>(&self, def_id: MaybeExternId, matcher: F) -> bool
214    where
215        F: Fn(&Path) -> bool,
216    {
217        let def_id = def_id.local_id();
218        let tcx = self.genv.tcx();
219        let span = tcx.def_span(def_id);
220        let sm = tcx.sess.source_map();
221        let FileName::Real(file_name) = sm.span_to_filename(span) else { return true };
222        let mut file_path = file_name.local_path_if_available();
223
224        // If the path is absolute try to normalize it to be relative to the working_dir
225        if file_path.is_absolute() {
226            let working_dir = tcx.sess.opts.working_dir.local_path_if_available();
227            let Ok(p) = file_path.strip_prefix(working_dir) else { return true };
228            file_path = p;
229        }
230
231        matcher(file_path)
232    }
233
234    fn matches_pos(&self, def_id: MaybeExternId, line: usize, col: usize) -> bool {
235        let def_id = def_id.local_id();
236        let tcx = self.genv.tcx();
237        let hir_id = tcx.local_def_id_to_hir_id(def_id);
238        let body_span = tcx.hir_span_with_body(hir_id);
239        let source_map = tcx.sess.source_map();
240        let lo_pos = source_map.lookup_char_pos(body_span.lo());
241        let start_line = lo_pos.line;
242        let start_col = lo_pos.col_display;
243        let hi_pos = source_map.lookup_char_pos(body_span.hi());
244        let end_line = hi_pos.line;
245        let end_col = hi_pos.col_display;
246
247        // is the line in the range of the body?
248        if start_line < end_line {
249            // multiple lines: check if the line is in the range
250            start_line <= line && line <= end_line
251        } else {
252            // single line: check if the line is the same and the column is in range
253            start_line == line && start_col <= col && col <= end_col
254        }
255    }
256
257    /// Check whether the `def_id` (or the file where `def_id` is defined)
258    /// is in the `include` pattern, and conservatively return `true` if
259    /// anything unexpected happens.
260    fn is_included(&self, def_id: MaybeExternId) -> bool {
261        let Some(pattern) = config::include_pattern() else { return true };
262        if self.matches_file_path(def_id, |path| pattern.glob.is_match(path)) {
263            return true;
264        }
265        if pattern.defs.iter().any(|def| self.matches_def(def_id, def)) {
266            return true;
267        }
268        if pattern.spans.iter().any(|pos| {
269            self.matches_file_path(def_id, |path| path.ends_with(&pos.file))
270                && self.matches_pos(def_id, pos.line, pos.column)
271        }) {
272            return true;
273        }
274        false
275    }
276
277    fn check_def_catching_bugs(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
278        let mut this = std::panic::AssertUnwindSafe(self);
279        let msg = format!("def_id: {:?}, span: {:?}", def_id, this.genv.tcx().def_span(def_id));
280        flux_common::bug::catch_bugs(&msg, move || this.check_def(def_id))?
281    }
282
283    fn check_def(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
284        let def_id = self.genv.maybe_extern_id(def_id);
285
286        // Dummy items generated for extern specs are excluded from metrics
287        if self.genv.is_dummy(def_id.local_id()) {
288            return Ok(());
289        }
290
291        let kind = self.genv.def_kind(def_id);
292
293        // For the purpose of metrics, we consider to be a *function* an item that
294        // 1. It's local, i.e., it's not an extern spec.
295        // 2. It's a free function (`DefKind::Fn`) or associated item (`DefKind::AssocFn`), and
296        // 3. It has a mir body
297        // In particular, this excludes closures (because they dont have the right `DefKind`) and
298        // trait methods without a default body.
299        let is_fn_with_body = def_id
300            .as_local()
301            .map(|local_id| {
302                matches!(kind, DefKind::Fn | DefKind::AssocFn)
303                    && self.genv.tcx().is_mir_available(local_id)
304            })
305            .unwrap_or(false);
306
307        metrics::incr_metric_if(is_fn_with_body, Metric::FnTotal);
308
309        if self.genv.ignored(def_id.local_id()) {
310            metrics::incr_metric_if(is_fn_with_body, Metric::FnIgnored);
311            return Ok(());
312        }
313        if !self.is_included(def_id) {
314            metrics::incr_metric_if(is_fn_with_body, Metric::FnTrusted);
315            return Ok(());
316        }
317
318        match kind {
319            DefKind::Fn | DefKind::AssocFn => {
320                // Make sure we run conversion and report errors even if we skip the function
321                force_conv(self.genv, def_id.resolved_id()).emit(&self.genv)?;
322                let Some(local_id) = def_id.as_local() else { return Ok(()) };
323                if is_fn_with_body {
324                    refineck::check_fn(self.genv, &mut self.cache, local_id)?;
325                }
326                Ok(())
327            }
328            DefKind::Enum => {
329                self.genv.check_wf(def_id.local_id()).emit(&self.genv)?;
330                self.genv.variants_of(def_id).emit(&self.genv)?;
331                let adt_def = self.genv.adt_def(def_id).emit(&self.genv)?;
332                let enum_def = self
333                    .genv
334                    .fhir_expect_item(def_id.local_id())
335                    .emit(&self.genv)?
336                    .expect_enum();
337                refineck::invariants::check_invariants(
338                    self.genv,
339                    &mut self.cache,
340                    def_id,
341                    enum_def.invariants,
342                    &adt_def,
343                )
344            }
345            DefKind::Struct => {
346                // We check invariants for `struct` in `check_constructor` (i.e. when the struct is built).
347                // However, we leave the below code in to force the queries that do the conversions that check
348                // for ill-formed annotations e.g. see tests/tests/neg/error_messages/annot_check/struct_error.rs
349                self.genv.check_wf(def_id.local_id()).emit(&self.genv)?;
350                self.genv.adt_def(def_id).emit(&self.genv)?;
351                self.genv.variants_of(def_id).emit(&self.genv)?;
352                let _struct_def = self
353                    .genv
354                    .fhir_expect_item(def_id.local_id())
355                    .emit(&self.genv)?
356                    .expect_struct();
357                Ok(())
358            }
359            DefKind::Impl { of_trait } => {
360                self.genv.check_wf(def_id.local_id()).emit(&self.genv)?;
361                if of_trait {
362                    refineck::compare_impl_item::check_impl_against_trait(self.genv, def_id)
363                        .emit(&self.genv)?;
364                }
365                Ok(())
366            }
367            DefKind::TyAlias => {
368                self.genv.check_wf(def_id.local_id()).emit(&self.genv)?;
369                self.genv.type_of(def_id).emit(&self.genv)?;
370                Ok(())
371            }
372            DefKind::Trait => {
373                self.genv.check_wf(def_id.local_id()).emit(&self.genv)?;
374                Ok(())
375            }
376            _ => Ok(()),
377        }
378    }
379}
380
381fn force_conv(genv: GlobalEnv, def_id: DefId) -> QueryResult {
382    genv.generics_of(def_id)?;
383    genv.refinement_generics_of(def_id)?;
384    genv.predicates_of(def_id)?;
385    genv.fn_sig(def_id)?;
386    Ok(())
387}
388
389fn mir_borrowck<'tcx>(
390    tcx: TyCtxt<'tcx>,
391    def_id: LocalDefId,
392) -> query::queries::mir_borrowck::ProvidedValue<'tcx> {
393    let bodies_with_facts = rustc_borrowck::consumers::get_bodies_with_borrowck_facts(
394        tcx,
395        def_id,
396        ConsumerOptions::RegionInferenceContext,
397    );
398    for (def_id, body_with_facts) in bodies_with_facts {
399        // SAFETY: This is safe because we are feeding in the same `tcx` that is
400        // going to be used as a witness when pulling out the data.
401        unsafe {
402            flux_common::mir_storage::store_mir_body(tcx, def_id, body_with_facts);
403        }
404    }
405    let mut providers = query::Providers::default();
406    rustc_borrowck::provide(&mut providers);
407    let original_mir_borrowck = providers.mir_borrowck;
408    original_mir_borrowck(tcx, def_id)
409}
flux_driver/callbacks.rs

flux_driver/
callbacks.rs
