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
48    fn after_analysis(&mut self, compiler: &Compiler, tcx: TyCtxt<'_>) -> Compilation {
49        self.verify(compiler, tcx);
50        if config::full_compilation() { Compilation::Continue } else { Compilation::Stop }
51    }
52}
53
54impl FluxCallbacks {
55    fn verify(&self, compiler: &Compiler, tcx: TyCtxt<'_>) {
56        if compiler.sess.dcx().has_errors().is_some() {
57            return;
58        }
59
60        let sess = FluxSession::new(
61            &tcx.sess.opts,
62            tcx.sess.psess.clone_source_map(),
63            rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false),
64        );
65
66        let mut providers = Providers::default();
67        flux_desugar::provide(&mut providers);
68        flux_fhir_analysis::provide(&mut providers);
69        providers.collect_specs = collect_specs;
70
71        let cstore = CStore::load(tcx, &sess);
72        let arena = fhir::Arena::new();
73        GlobalEnv::enter(tcx, &sess, Box::new(cstore), &arena, providers, |genv| {
74            let result = metrics::time_it(TimingKind::Total, || check_crate(genv));
75            if result.is_ok() {
76                encode_and_save_metadata(genv);
77            }
78            lean_encoding::finalize(genv).unwrap_or(());
79        });
80        let _ = metrics::print_and_dump_timings(tcx);
81        sess.finish_diagnostics();
82    }
83}
84
85fn check_crate(genv: GlobalEnv) -> Result<(), ErrorGuaranteed> {
86    tracing::info_span!("check_crate").in_scope(move || {
87        tracing::info!("Callbacks::check_wf");
88        // Query qualifiers and spec funcs to report wf errors
89        let _ = genv.qualifiers().emit(&genv)?;
90        let _ = genv.normalized_defns(LOCAL_CRATE);
91
92        let mut ck = CrateChecker::new(genv);
93
94        // Iterate over all def ids including dummy items for extern specs
95        let result = genv
96            .tcx()
97            .iter_local_def_id()
98            .try_for_each_exhaust(|def_id| ck.check_def_catching_bugs(def_id));
99
100        if config::lean().is_check() || config::lean().is_emit() {
101            lean_encoding::finalize(genv)
102                .unwrap_or_else(|err| bug!("error running lean-check {err:?}"));
103        }
104
105        let lean_result = if config::lean().is_check() {
106            genv.iter_local_def_id().try_for_each_exhaust(|def_id| {
107                if genv.proven_externally(def_id).is_some() {
108                    let key = lean_task_key(genv.tcx(), def_id.to_def_id());
109                    // Skip proof check if previously verified successfully.
110                    if config::is_cache_enabled()
111                        && ck
112                            .cache
113                            .lookup_by_key(&key)
114                            .map(|r| matches!(r.lean_status, LeanStatus::Valid))
115                            .unwrap_or(false)
116                    {
117                        return Ok(());
118                    }
119                    lean_encoding::check_proof(genv, def_id.to_def_id())?;
120                    // Mark as valid in cache so future runs skip re-verification.
121                    ck.cache
122                        .update_result_by_key(&key, |r| r.lean_status = LeanStatus::Valid);
123                    Ok(())
124                } else {
125                    Ok(())
126                }
127            })
128        } else {
129            Ok(())
130        };
131
132        ck.cache.save().unwrap_or(());
133
134        tracing::info!("Callbacks::check_crate");
135
136        result.and(lean_result)
137    })
138}
139
140fn collect_specs(genv: GlobalEnv) -> Specs {
141    match SpecCollector::collect(genv.tcx(), genv.sess()) {
142        Ok(specs) => specs,
143        Err(err) => {
144            genv.sess().abort(err);
145        }
146    }
147}
148
149fn encode_and_save_metadata(genv: GlobalEnv) {
150    // We only save metadata when `--emit=metadata` is passed as an argument. In this case, we save
151    // the `.fluxmeta` file alongside the `.rmeta` file. This setup works for `cargo flux`, which
152    // wraps `cargo check` and always passes `--emit=metadata`. Tests also explicitly pass this flag.
153    let tcx = genv.tcx();
154    if tcx
155        .output_filenames(())
156        .outputs
157        .contains_key(&OutputType::Metadata)
158    {
159        let path = flux_metadata::filename_for_metadata(tcx);
160        flux_metadata::encode_metadata(genv, path.as_path());
161    }
162}
163
164struct CrateChecker<'genv, 'tcx> {
165    genv: GlobalEnv<'genv, 'tcx>,
166    cache: FixQueryCache,
167}
168
169impl<'genv, 'tcx> CrateChecker<'genv, 'tcx> {
170    fn new(genv: GlobalEnv<'genv, 'tcx>) -> Self {
171        Self { genv, cache: QueryCache::load() }
172    }
173
174    fn check_def_catching_bugs(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
175        let mut this = std::panic::AssertUnwindSafe(self);
176        let msg = format!("def_id: {:?}, span: {:?}", def_id, this.genv.tcx().def_span(def_id));
177        flux_common::bug::catch_bugs(&msg, move || this.check_def(def_id))?
178    }
179
180    fn check_def(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
181        let genv = self.genv;
182        let def_id = genv.maybe_extern_id(def_id);
183
184        // Dummy items generated for extern specs are excluded from metrics
185        if genv.is_dummy(def_id.local_id()) {
186            return Ok(());
187        }
188
189        let kind = genv.def_kind(def_id);
190
191        // For the purpose of metrics, we consider to be a *function* an item that
192        // 1. It's local, i.e., it's not an extern spec.
193        // 2. It's a free function (`DefKind::Fn`) or associated item (`DefKind::AssocFn`), and
194        // 3. It has a mir body
195        // In particular, this excludes closures (because they dont have the right `DefKind`) and
196        // trait methods without a default body.
197        let is_fn_with_body = def_id
198            .as_local()
199            .map(|local_id| {
200                matches!(kind, DefKind::Fn | DefKind::AssocFn)
201                    && genv.tcx().is_mir_available(local_id)
202            })
203            .unwrap_or(false);
204
205        metrics::incr_metric_if(is_fn_with_body, Metric::FnTotal);
206
207        if genv.ignored(def_id.local_id()) {
208            metrics::incr_metric_if(is_fn_with_body, Metric::FnIgnored);
209            return Ok(());
210        }
211        if !self.genv.included(def_id) {
212            metrics::incr_metric_if(is_fn_with_body, Metric::FnTrusted);
213            return Ok(());
214        }
215
216        trigger_queries(genv, def_id).emit(&genv)?;
217
218        match kind {
219            DefKind::Fn | DefKind::AssocFn => {
220                let Some(local_id) = def_id.as_local() else { return Ok(()) };
221                if is_fn_with_body {
222                    refineck::check_fn(genv, &mut self.cache, local_id)?;
223                }
224            }
225            DefKind::Enum => {
226                let adt_def = genv.adt_def(def_id).emit(&genv)?;
227                let enum_def = genv
228                    .fhir_expect_item(def_id.local_id())
229                    .emit(&genv)?
230                    .expect_enum();
231                refineck::invariants::check_invariants(
232                    genv,
233                    &mut self.cache,
234                    def_id,
235                    enum_def.invariants,
236                    &adt_def,
237                )?;
238            }
239            DefKind::Struct => {
240                // We check invariants for `struct` in `check_constructor` (i.e. when the struct is built),
241                // so nothing to do here.
242            }
243            DefKind::Impl { of_trait } => {
244                if of_trait {
245                    refineck::compare_impl_item::check_impl_against_trait(genv, def_id)
246                        .emit(&genv)?;
247                }
248            }
249            DefKind::TyAlias => {}
250            DefKind::Trait => {}
251            DefKind::Static { .. } => {
252                if let StaticInfo::Known(ty) = genv.static_info(def_id).emit(&genv)?
253                    && let Some(local_id) = def_id.as_local()
254                {
255                    refineck::check_static(genv, &mut self.cache, local_id, ty)?;
256                }
257            }
258            _ => (),
259        }
260        Ok(())
261    }
262}
263
264/// Triggers queries for the given `def_id` to mark it as "reached" for metadata encoding.
265///
266/// This function ensures that all relevant queries for a definition are triggered upfront,
267/// so the item and its associated data will be included in the encoded metadata. Without this,
268/// items might be missing from the metadata (extern specs in particular which are not otherwise "checked"),
269/// causing errors when dependent crates try to use them.
270fn trigger_queries(genv: GlobalEnv, def_id: MaybeExternId) -> QueryResult {
271    match genv.def_kind(def_id) {
272        DefKind::Trait => {
273            genv.generics_of(def_id)?;
274            genv.predicates_of(def_id)?;
275            genv.refinement_generics_of(def_id)?;
276        }
277        DefKind::Impl { .. } => {
278            genv.generics_of(def_id)?;
279            genv.predicates_of(def_id)?;
280            genv.refinement_generics_of(def_id)?;
281        }
282        DefKind::Fn | DefKind::AssocFn => {
283            genv.generics_of(def_id)?;
284            genv.refinement_generics_of(def_id)?;
285            genv.predicates_of(def_id)?;
286            genv.fn_sig(def_id)?;
287        }
288        DefKind::Ctor(_, CtorKind::Fn) => {
289            genv.generics_of(def_id)?;
290            genv.refinement_generics_of(def_id)?;
291            // We don't report the error because it can raise a `QueryErr::OpaqueStruct`,  which
292            // should be reported at the use site.
293            let _ = genv.fn_sig(def_id);
294        }
295        DefKind::Enum | DefKind::Struct => {
296            genv.generics_of(def_id)?;
297            genv.predicates_of(def_id)?;
298            genv.refinement_generics_of(def_id)?;
299            genv.adt_def(def_id)?;
300            genv.adt_sort_def_of(def_id)?;
301            genv.variants_of(def_id)?;
302            genv.type_of(def_id)?;
303        }
304        DefKind::TyAlias => {
305            genv.generics_of(def_id)?;
306            genv.predicates_of(def_id)?;
307            genv.refinement_generics_of(def_id)?;
308            genv.type_of(def_id)?;
309        }
310        DefKind::OpaqueTy => {
311            genv.generics_of(def_id)?;
312            genv.predicates_of(def_id)?;
313            genv.item_bounds(def_id)?;
314            genv.refinement_generics_of(def_id)?;
315        }
316        _ => {}
317    }
318    Ok(())
319}
320
321fn mir_borrowck<'tcx>(
322    tcx: TyCtxt<'tcx>,
323    def_id: LocalDefId,
324) -> query::queries::mir_borrowck::ProvidedValue<'tcx> {
325    let bodies_with_facts = rustc_borrowck::consumers::get_bodies_with_borrowck_facts(
326        tcx,
327        def_id,
328        ConsumerOptions::RegionInferenceContext,
329    );
330    for (def_id, body_with_facts) in bodies_with_facts {
331        // SAFETY: This is safe because we are feeding in the same `tcx` that is
332        // going to be used as a witness when pulling out the data.
333        unsafe {
334            flux_common::mir_storage::store_mir_body(tcx, def_id, body_with_facts);
335        }
336    }
337    let mut providers = query::Providers::default();
338    rustc_borrowck::provide(&mut providers);
339    let original_mir_borrowck = providers.mir_borrowck;
340    original_mir_borrowck(tcx, def_id)
341}
flux_driver/callbacks.rs

flux_driver/
callbacks.rs
