flux_driver/
callbacks.rs

1use flux_common::{bug, cache::QueryCache, iter::IterExt, result::ResultExt};
2use flux_config::{self as config};
3use flux_errors::FluxSession;
4use flux_infer::{
5    fixpoint_encoding::{FixQueryCache, LeanStatus, lean_task_key},
6    lean_encoding,
7};
8use flux_metadata::CStore;
9use flux_middle::{
10    Specs,
11    def_id::MaybeExternId,
12    fhir::{self},
13    global_env::GlobalEnv,
14    metrics::{self, Metric, TimingKind},
15    queries::{Providers, QueryResult},
16    rty::StaticInfo,
17};
18use flux_refineck as refineck;
19use rustc_borrowck::consumers::ConsumerOptions;
20use rustc_driver::{Callbacks, Compilation};
21use rustc_errors::ErrorGuaranteed;
22use rustc_hir::{
23    def::{CtorKind, DefKind},
24    def_id::{LOCAL_CRATE, LocalDefId},
25};
26use rustc_interface::interface::Compiler;
27use rustc_middle::{query, ty::TyCtxt};
28use rustc_session::config::OutputType;
29
30use crate::{DEFAULT_LOCALE_RESOURCES, collector::SpecCollector};
31
32#[derive(Default)]
33pub struct FluxCallbacks;
34
35impl Callbacks for FluxCallbacks {
36    fn config(&mut self, config: &mut rustc_interface::interface::Config) {
37        assert!(config.override_queries.is_none());
38
39        config.override_queries = Some(|_, local| {
40            local.mir_borrowck = mir_borrowck;
41        });
42        // this should always be empty otherwise something changed in rustc and all our assumptions
43        // about symbol interning are wrong.
44        assert!(config.extra_symbols.is_empty());
45        config.extra_symbols = flux_syntax::symbols::PREDEFINED_FLUX_SYMBOLS.to_vec();
46
47        if flux_config::std_extern_specs() {
48            inject_std_extern_specs(config);
49        }
50    }
51
52    fn after_analysis(&mut self, compiler: &Compiler, tcx: TyCtxt<'_>) -> Compilation {
53        self.verify(compiler, tcx);
54        if config::full_compilation() { Compilation::Continue } else { Compilation::Stop }
55    }
56}
57
58impl FluxCallbacks {
59    fn verify(&self, compiler: &Compiler, tcx: TyCtxt<'_>) {
60        if compiler.sess.dcx().has_errors().is_some() {
61            return;
62        }
63
64        let sess = FluxSession::new(
65            &tcx.sess.opts,
66            tcx.sess.psess.clone_source_map(),
67            rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false),
68        );
69
70        let mut providers = Providers::default();
71        flux_opt::provide(&mut providers);
72        flux_desugar::provide(&mut providers);
73        flux_fhir_analysis::provide(&mut providers);
74        providers.collect_specs = collect_specs;
75
76        let cstore = CStore::load(tcx, &sess);
77        let arena = fhir::Arena::new();
78        GlobalEnv::enter(tcx, &sess, Box::new(cstore), &arena, providers, |genv| {
79            let result = metrics::time_it(TimingKind::Total, || check_crate(genv));
80            if result.is_ok() {
81                encode_and_save_metadata(genv);
82            }
83            lean_encoding::finalize(genv).unwrap_or(());
84        });
85        let _ = metrics::print_and_dump_timings(tcx);
86        sess.finish_diagnostics();
87    }
88}
89
90fn load_extern_specs() -> Vec<(String, std::path::PathBuf)> {
91    use flux_sysroot::SysrootManifest;
92    let Some(sysroot) = config::sysroot() else { return vec![] };
93    let Ok(content) = std::fs::read_to_string(sysroot.join("sysroot.toml")) else { return vec![] };
94    let Ok(manifest) = toml::from_str::<SysrootManifest>(&content) else { return vec![] };
95    manifest
96        .extern_specs
97        .into_iter()
98        .map(|(name, rmeta)| (name, sysroot.join(&rmeta)))
99        .collect()
100}
101
102fn inject_std_extern_specs(config: &mut rustc_interface::interface::Config) {
103    use std::collections::{BTreeMap, BTreeSet};
104
105    use rustc_session::{
106        config::{ExternEntry, ExternLocation, Externs},
107        utils::CanonicalizedPath,
108    };
109
110    let specs = load_extern_specs();
111    if specs.is_empty() {
112        return;
113    }
114
115    let mut map: BTreeMap<String, ExternEntry> = config
116        .opts
117        .externs
118        .iter()
119        .map(|(k, v)| (k.clone(), v.clone()))
120        .collect();
121
122    for (crate_name, rmeta_path) in specs {
123        let entry = ExternEntry {
124            location: ExternLocation::ExactPaths(BTreeSet::from([CanonicalizedPath::new(
125                rmeta_path,
126            )])),
127            is_private_dep: false,
128            add_prelude: true,
129            nounused_dep: true,
130            force: true,
131        };
132        map.insert(crate_name, entry);
133    }
134
135    config.opts.externs = Externs::new(map);
136}
137
138fn check_crate(genv: GlobalEnv) -> Result<(), ErrorGuaranteed> {
139    tracing::info_span!("check_crate").in_scope(move || {
140        tracing::info!("Callbacks::check_wf");
141        // Query qualifiers and spec funcs to report wf errors
142        let _ = genv.qualifiers().emit(&genv)?;
143        let _ = genv.normalized_defns(LOCAL_CRATE);
144
145        let mut ck = CrateChecker::new(genv);
146
147        // Iterate over all def ids including dummy items for extern specs
148        let result = genv
149            .tcx()
150            .iter_local_def_id()
151            .try_for_each_exhaust(|def_id| ck.check_def_catching_bugs(def_id));
152
153        if config::lean().is_check() || config::lean().is_emit() {
154            lean_encoding::finalize(genv)
155                .unwrap_or_else(|err| bug!("error running lean-check {err:?}"));
156        }
157
158        let lean_result = if config::lean().is_check() {
159            genv.iter_local_def_id().try_for_each_exhaust(|def_id| {
160                // Skip proof check if not included
161                if !genv.included(genv.maybe_extern_id(def_id)) {
162                    return Ok(());
163                }
164                if genv.proven_externally(def_id).is_some() {
165                    let key = lean_task_key(genv.tcx(), def_id.to_def_id());
166                    // Skip proof check if previously verified successfully.
167                    if config::is_cache_enabled()
168                        && ck
169                            .cache
170                            .lookup_by_key(&key)
171                            .map(|r| matches!(r.lean_status, LeanStatus::Valid))
172                            .unwrap_or(false)
173                    {
174                        return Ok(());
175                    }
176                    lean_encoding::check_proof(genv, def_id.to_def_id())?;
177                    // Mark as valid in cache so future runs skip re-verification.
178                    ck.cache
179                        .update_result_by_key(&key, |r| r.lean_status = LeanStatus::Valid);
180                    Ok(())
181                } else {
182                    Ok(())
183                }
184            })
185        } else {
186            Ok(())
187        };
188
189        ck.cache.save().unwrap_or(());
190
191        tracing::info!("Callbacks::check_crate");
192
193        result.and(lean_result)
194    })
195}
196
197fn collect_specs(genv: GlobalEnv) -> Specs {
198    match SpecCollector::collect(genv.tcx(), genv.sess()) {
199        Ok(specs) => specs,
200        Err(err) => {
201            genv.sess().abort(err);
202        }
203    }
204}
205
206fn encode_and_save_metadata(genv: GlobalEnv) {
207    // We only save metadata when `--emit=metadata` is passed as an argument. In this case, we save
208    // the `.fluxmeta` file alongside the `.rmeta` file. This setup works for `cargo flux`, which
209    // wraps `cargo check` and always passes `--emit=metadata`. Tests also explicitly pass this flag.
210    let tcx = genv.tcx();
211    if tcx
212        .output_filenames(())
213        .outputs
214        .contains_key(&OutputType::Metadata)
215    {
216        let path = flux_metadata::filename_for_metadata(tcx);
217        flux_metadata::encode_metadata(genv, path.as_path());
218    }
219}
220
221struct CrateChecker<'genv, 'tcx> {
222    genv: GlobalEnv<'genv, 'tcx>,
223    cache: FixQueryCache,
224}
225
226impl<'genv, 'tcx> CrateChecker<'genv, 'tcx> {
227    fn new(genv: GlobalEnv<'genv, 'tcx>) -> Self {
228        Self { genv, cache: QueryCache::load() }
229    }
230
231    fn check_def_catching_bugs(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
232        let mut this = std::panic::AssertUnwindSafe(self);
233        let msg = format!("def_id: {:?}, span: {:?}", def_id, this.genv.tcx().def_span(def_id));
234        flux_common::bug::catch_bugs(&msg, move || this.check_def(def_id))?
235    }
236
237    fn check_def(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
238        let genv = self.genv;
239        let def_id = genv.maybe_extern_id(def_id);
240
241        // Dummy items generated for extern specs are excluded from metrics
242        if genv.is_dummy(def_id.local_id()) {
243            return Ok(());
244        }
245
246        let kind = genv.def_kind(def_id);
247
248        // For the purpose of metrics, we consider to be a *function* an item that
249        // 1. It's local, i.e., it's not an extern spec.
250        // 2. It's a free function (`DefKind::Fn`) or associated item (`DefKind::AssocFn`), and
251        // 3. It has a mir body
252        // In particular, this excludes closures (because they dont have the right `DefKind`) and
253        // trait methods without a default body.
254        let is_fn_with_body = def_id
255            .as_local()
256            .map(|local_id| {
257                matches!(kind, DefKind::Fn | DefKind::AssocFn)
258                    && genv.tcx().is_mir_available(local_id)
259            })
260            .unwrap_or(false);
261
262        metrics::incr_metric_if(is_fn_with_body, Metric::FnTotal);
263
264        if genv.ignored(def_id.local_id()) {
265            metrics::incr_metric_if(is_fn_with_body, Metric::FnIgnored);
266            return Ok(());
267        }
268        if !self.genv.included(def_id) {
269            metrics::incr_metric_if(is_fn_with_body, Metric::FnTrusted);
270            return Ok(());
271        }
272
273        trigger_queries(genv, def_id).emit(&genv)?;
274
275        match kind {
276            DefKind::Fn | DefKind::AssocFn => {
277                let Some(local_id) = def_id.as_local() else { return Ok(()) };
278                if is_fn_with_body {
279                    refineck::check_fn(genv, &mut self.cache, local_id)?;
280                }
281            }
282            DefKind::Enum => {
283                let adt_def = genv.adt_def(def_id).emit(&genv)?;
284                let enum_def = genv
285                    .fhir_expect_item(def_id.local_id())
286                    .emit(&genv)?
287                    .expect_enum();
288                refineck::invariants::check_invariants(
289                    genv,
290                    &mut self.cache,
291                    def_id,
292                    enum_def.invariants,
293                    &adt_def,
294                )?;
295            }
296            DefKind::Struct => {
297                // We check invariants for `struct` in `check_constructor` (i.e. when the struct is built),
298                // so nothing to do here.
299            }
300            DefKind::Impl { of_trait } => {
301                if of_trait {
302                    refineck::compare_impl_item::check_impl_against_trait(genv, def_id)
303                        .emit(&genv)?;
304                }
305            }
306            DefKind::TyAlias => {}
307            DefKind::Trait => {}
308            DefKind::Static { .. } => {
309                if let StaticInfo::Known(ty) = genv.static_info(def_id).emit(&genv)?
310                    && let Some(local_id) = def_id.as_local()
311                {
312                    refineck::check_static(genv, &mut self.cache, local_id, ty)?;
313                }
314            }
315            _ => (),
316        }
317        Ok(())
318    }
319}
320
321/// Triggers queries for the given `def_id` to mark it as "reached" for metadata encoding.
322///
323/// This function ensures that all relevant queries for a definition are triggered upfront,
324/// so the item and its associated data will be included in the encoded metadata. Without this,
325/// items might be missing from the metadata (extern specs in particular which are not otherwise "checked"),
326/// causing errors when dependent crates try to use them.
327fn trigger_queries(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult {
328    match genv.def_kind(def_id) {
329        DefKind::Trait => {
330            genv.generics_of(def_id)?;
331            genv.predicates_of(def_id)?;
332            genv.refinement_generics_of(def_id)?;
333        }
334        DefKind::Impl { .. } => {
335            genv.generics_of(def_id)?;
336            genv.predicates_of(def_id)?;
337            genv.refinement_generics_of(def_id)?;
338        }
339        DefKind::Fn | DefKind::AssocFn => {
340            genv.generics_of(def_id)?;
341            genv.refinement_generics_of(def_id)?;
342            genv.predicates_of(def_id)?;
343            genv.fn_sig(def_id)?;
344        }
345        DefKind::Ctor(_, CtorKind::Fn) => {
346            genv.generics_of(def_id)?;
347            genv.refinement_generics_of(def_id)?;
348            // We don't report the error because it can raise a `QueryErr::OpaqueStruct`,  which
349            // should be reported at the use site.
350            let _ = genv.fn_sig(def_id);
351        }
352        DefKind::Enum | DefKind::Struct => {
353            genv.generics_of(def_id)?;
354            genv.predicates_of(def_id)?;
355            genv.refinement_generics_of(def_id)?;
356            genv.adt_def(def_id)?;
357            genv.adt_sort_def_of(def_id)?;
358            genv.variants_of(def_id)?;
359            genv.type_of(def_id)?;
360        }
361        DefKind::TyAlias => {
362            genv.generics_of(def_id)?;
363            genv.predicates_of(def_id)?;
364            genv.refinement_generics_of(def_id)?;
365            genv.type_of(def_id)?;
366        }
367        DefKind::OpaqueTy => {
368            genv.generics_of(def_id)?;
369            genv.predicates_of(def_id)?;
370            genv.item_bounds(def_id)?;
371            genv.refinement_generics_of(def_id)?;
372        }
373        _ => {}
374    }
375    Ok(())
376}
377
378fn mir_borrowck<'tcx>(
379    tcx: TyCtxt<'tcx>,
380    def_id: LocalDefId,
381) -> query::queries::mir_borrowck::ProvidedValue<'tcx> {
382    let bodies_with_facts = rustc_borrowck::consumers::get_bodies_with_borrowck_facts(
383        tcx,
384        def_id,
385        ConsumerOptions::RegionInferenceContext,
386    );
387    for (def_id, body_with_facts) in bodies_with_facts {
388        // SAFETY: This is safe because we are feeding in the same `tcx` that is
389        // going to be used as a witness when pulling out the data.
390        unsafe {
391            flux_common::mir_storage::store_mir_body(tcx, def_id, body_with_facts);
392        }
393    }
394    let mut providers = query::Providers::default();
395    rustc_borrowck::provide(&mut providers);
396    let original_mir_borrowck = providers.mir_borrowck;
397    original_mir_borrowck(tcx, def_id)
398}
flux_driver/callbacks.rs

flux_driver/
callbacks.rs
