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                    fun_defs.push(
171                        ecx.fun_def_to_fixpoint(spec_func.def_id.to_def_id(), &mut scx)
172                            .unwrap(),
173                    );
174                }
175                FluxItem::Func(spec_func) => {
176                    opaque_fun_defs
177                        .push(ecx.fun_decl_to_fixpoint(spec_func.def_id.to_def_id(), &mut scx));
178                }
179                _ => {}
180            }
181        }
182        let opaque_sorts = scx.user_sorts_to_fixpoint(self.genv);
183        let adt_defs = scx.encode_data_decls(self.genv).unwrap();
184        if !opaque_sorts.is_empty()
185            || !opaque_fun_defs.is_empty()
186            || !adt_defs.is_empty()
187            || !fun_defs.is_empty()
188        {
189            let encoder = LeanEncoder::new(
190                self.genv,
191                std::path::Path::new("./"),
192                "lean_proofs".to_string(),
193                "Defs".to_string(),
194            );
195            encoder
196                .encode_defs(&opaque_sorts, &opaque_fun_defs, &adt_defs, &fun_defs)
197                .unwrap();
198        }
199        Ok(())
200    }
201
202    fn matches_def(&self, def_id: MaybeExternId, def: &str) -> bool {
203        // Does this def_id's name contain `fn_name`?
204        let def_path = self.genv.tcx().def_path_str(def_id.local_id());
205        def_path.contains(def)
206    }
207
208    fn matches_file_path<F>(&self, def_id: MaybeExternId, matcher: F) -> bool
209    where
210        F: Fn(&Path) -> bool,
211    {
212        let def_id = def_id.local_id();
213        let tcx = self.genv.tcx();
214        let span = tcx.def_span(def_id);
215        let sm = tcx.sess.source_map();
216        let FileName::Real(file_name) = sm.span_to_filename(span) else { return true };
217        let mut file_path = file_name.local_path_if_available();
218
219        // If the path is absolute try to normalize it to be relative to the working_dir
220        if file_path.is_absolute() {
221            let working_dir = tcx.sess.opts.working_dir.local_path_if_available();
222            let Ok(p) = file_path.strip_prefix(working_dir) else { return true };
223            file_path = p;
224        }
225
226        matcher(file_path)
227    }
228
229    fn matches_pos(&self, def_id: MaybeExternId, line: usize, col: usize) -> bool {
230        let def_id = def_id.local_id();
231        let tcx = self.genv.tcx();
232        let hir_id = tcx.local_def_id_to_hir_id(def_id);
233        let body_span = tcx.hir_span_with_body(hir_id);
234        let source_map = tcx.sess.source_map();
235        let lo_pos = source_map.lookup_char_pos(body_span.lo());
236        let start_line = lo_pos.line;
237        let start_col = lo_pos.col_display;
238        let hi_pos = source_map.lookup_char_pos(body_span.hi());
239        let end_line = hi_pos.line;
240        let end_col = hi_pos.col_display;
241
242        // is the line in the range of the body?
243        if start_line < end_line {
244            // multiple lines: check if the line is in the range
245            start_line <= line && line <= end_line
246        } else {
247            // single line: check if the line is the same and the column is in range
248            start_line == line && start_col <= col && col <= end_col
249        }
250    }
251
252    /// Check whether the `def_id` (or the file where `def_id` is defined)
253    /// is in the `include` pattern, and conservatively return `true` if
254    /// anything unexpected happens.
255    fn is_included(&self, def_id: MaybeExternId) -> bool {
256        let Some(pattern) = config::include_pattern() else { return true };
257        if self.matches_file_path(def_id, |path| pattern.glob.is_match(path)) {
258            return true;
259        }
260        if pattern.defs.iter().any(|def| self.matches_def(def_id, def)) {
261            return true;
262        }
263        if pattern.spans.iter().any(|pos| {
264            self.matches_file_path(def_id, |path| path.ends_with(&pos.file))
265                && self.matches_pos(def_id, pos.line, pos.column)
266        }) {
267            return true;
268        }
269        false
270    }
271
272    fn check_def_catching_bugs(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
273        let mut this = std::panic::AssertUnwindSafe(self);
274        let msg = format!("def_id: {:?}, span: {:?}", def_id, this.genv.tcx().def_span(def_id));
275        flux_common::bug::catch_bugs(&msg, move || this.check_def(def_id))?
276    }
277
278    fn check_def(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
279        let def_id = self.genv.maybe_extern_id(def_id);
280
281        // Dummy items generated for extern specs are excluded from metrics
282        if self.genv.is_dummy(def_id.local_id()) {
283            return Ok(());
284        }
285
286        let kind = self.genv.def_kind(def_id);
287        metrics::incr_metric_if(kind.is_fn_like(), Metric::FnTotal);
288
289        if self.genv.ignored(def_id.local_id()) {
290            metrics::incr_metric_if(kind.is_fn_like(), Metric::FnIgnored);
291            return Ok(());
292        }
293        if !self.is_included(def_id) {
294            metrics::incr_metric_if(kind.is_fn_like(), Metric::FnTrusted);
295            return Ok(());
296        }
297
298        match kind {
299            DefKind::Fn | DefKind::AssocFn => {
300                // Make sure we run conversion and report errors even if we skip the function
301                force_conv(self.genv, def_id.resolved_id()).emit(&self.genv)?;
302                let Some(local_id) = def_id.as_local() else { return Ok(()) };
303                refineck::check_fn(self.genv, &mut self.cache, local_id)
304            }
305            DefKind::Enum => {
306                self.genv.check_wf(def_id.local_id()).emit(&self.genv)?;
307                self.genv.variants_of(def_id).emit(&self.genv)?;
308                let adt_def = self.genv.adt_def(def_id).emit(&self.genv)?;
309                let enum_def = self
310                    .genv
311                    .fhir_expect_item(def_id.local_id())
312                    .emit(&self.genv)?
313                    .expect_enum();
314                refineck::invariants::check_invariants(
315                    self.genv,
316                    &mut self.cache,
317                    def_id,
318                    enum_def.invariants,
319                    &adt_def,
320                )
321            }
322            DefKind::Struct => {
323                // We check invariants for `struct` in `check_constructor` (i.e. when the struct is built).
324                // However, we leave the below code in to force the queries that do the conversions that check
325                // for ill-formed annotations e.g. see tests/tests/neg/error_messages/annot_check/struct_error.rs
326                self.genv.check_wf(def_id.local_id()).emit(&self.genv)?;
327                self.genv.adt_def(def_id).emit(&self.genv)?;
328                self.genv.variants_of(def_id).emit(&self.genv)?;
329                let _struct_def = self
330                    .genv
331                    .fhir_expect_item(def_id.local_id())
332                    .emit(&self.genv)?
333                    .expect_struct();
334                Ok(())
335            }
336            DefKind::Impl { of_trait } => {
337                self.genv.check_wf(def_id.local_id()).emit(&self.genv)?;
338                if of_trait {
339                    refineck::compare_impl_item::check_impl_against_trait(self.genv, def_id)
340                        .emit(&self.genv)?;
341                }
342                Ok(())
343            }
344            DefKind::TyAlias => {
345                self.genv.check_wf(def_id.local_id()).emit(&self.genv)?;
346                self.genv.type_of(def_id).emit(&self.genv)?;
347                Ok(())
348            }
349            DefKind::Trait => {
350                self.genv.check_wf(def_id.local_id()).emit(&self.genv)?;
351                Ok(())
352            }
353            _ => Ok(()),
354        }
355    }
356}
357
358fn force_conv(genv: GlobalEnv, def_id: DefId) -> QueryResult {
359    genv.generics_of(def_id)?;
360    genv.refinement_generics_of(def_id)?;
361    genv.predicates_of(def_id)?;
362    genv.fn_sig(def_id)?;
363    Ok(())
364}
365
366fn mir_borrowck<'tcx>(
367    tcx: TyCtxt<'tcx>,
368    def_id: LocalDefId,
369) -> query::queries::mir_borrowck::ProvidedValue<'tcx> {
370    let bodies_with_facts = rustc_borrowck::consumers::get_bodies_with_borrowck_facts(
371        tcx,
372        def_id,
373        ConsumerOptions::RegionInferenceContext,
374    );
375    for (def_id, body_with_facts) in bodies_with_facts {
376        // SAFETY: This is safe because we are feeding in the same `tcx` that is
377        // going to be used as a witness when pulling out the data.
378        unsafe {
379            flux_common::mir_storage::store_mir_body(tcx, def_id, body_with_facts);
380        }
381    }
382    let mut providers = query::Providers::default();
383    rustc_borrowck::provide(&mut providers);
384    let original_mir_borrowck = providers.mir_borrowck;
385    original_mir_borrowck(tcx, def_id)
386}
flux_driver/callbacks.rs

flux_driver/
callbacks.rs
