flux_driver/collector/
mod.rs

1mod annot_stats;
2mod detached_specs;
3mod extern_specs;
4
5use std::collections::HashMap;
6
7use annot_stats::Stats;
8use extern_specs::ExternSpecCollector;
9use flux_common::{
10    iter::IterExt,
11    result::{ErrorCollector, ResultExt},
12    tracked_span_assert_eq,
13};
14use flux_config::{self as config, OverflowMode, PartialInferOpts, SmtSolver};
15use flux_errors::{Errors, FluxSession};
16use flux_middle::{
17    Specs,
18    fhir::{Ignored, Trusted},
19};
20use flux_syntax::{ParseResult, ParseSess, surface};
21use itertools::Itertools;
22use rustc_ast::{MetaItemInner, MetaItemKind, tokenstream::TokenStream};
23use rustc_errors::ErrorGuaranteed;
24use rustc_hir::{
25    self as hir, Attribute, CRATE_OWNER_ID, EnumDef, ImplItemKind, Item, ItemKind, OwnerId,
26    VariantData,
27    def::DefKind,
28    def_id::{CRATE_DEF_ID, LocalDefId},
29};
30use rustc_middle::ty::TyCtxt;
31use rustc_span::{Span, Symbol, SyntaxContext};
32
33use crate::collector::detached_specs::DetachedSpecsCollector;
34type Result<T = ()> = std::result::Result<T, ErrorGuaranteed>;
35
36pub(crate) struct SpecCollector<'sess, 'tcx> {
37    tcx: TyCtxt<'tcx>,
38    parse_sess: ParseSess,
39    specs: Specs,
40    errors: Errors<'sess>,
41    stats: Stats,
42}
43
44macro_rules! attr_name {
45    ($kind:ident) => {{
46        let _ = FluxAttrKind::$kind;
47        stringify!($kind)
48    }};
49}
50
51impl<'tcx> hir::intravisit::Visitor<'tcx> for SpecCollector<'_, 'tcx> {
52    type NestedFilter = rustc_middle::hir::nested_filter::All;
53
54    fn maybe_tcx(&mut self) -> Self::MaybeTyCtxt {
55        self.tcx
56    }
57
58    fn visit_item(&mut self, item: &'tcx Item<'tcx>) {
59        let _ = self.collect_item(item);
60    }
61
62    fn visit_trait_item(&mut self, trait_item: &'tcx rustc_hir::TraitItem<'tcx>) {
63        let _ = self.collect_trait_item(trait_item);
64    }
65
66    fn visit_impl_item(&mut self, impl_item: &'tcx rustc_hir::ImplItem<'tcx>) {
67        let _ = self.collect_impl_item(impl_item);
68    }
69}
70
71impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
72    pub(crate) fn collect(tcx: TyCtxt<'tcx>, sess: &'a FluxSession) -> Result<Specs> {
73        let mut collector = Self {
74            tcx,
75            parse_sess: ParseSess::default(),
76            specs: Specs::default(),
77            errors: Errors::new(sess),
78            stats: Default::default(),
79        };
80
81        let _ = collector.collect_crate();
82        tcx.hir_walk_toplevel_module(&mut collector);
83
84        if config::annots() {
85            collector.stats.save(tcx).unwrap();
86        }
87
88        collector.errors.into_result()?;
89
90        Ok(collector.specs)
91    }
92
93    fn collect_crate(&mut self) -> Result {
94        let mut attrs = self.parse_attrs_and_report_dups(CRATE_DEF_ID)?;
95        self.collect_ignore_and_trusted(&mut attrs, CRATE_DEF_ID);
96        self.collect_infer_opts(&mut attrs, CRATE_DEF_ID);
97        DetachedSpecsCollector::collect(self, &mut attrs)?;
98
99        self.specs
100            .flux_items_by_parent
101            .entry(CRATE_OWNER_ID)
102            .or_default()
103            .extend(attrs.items());
104        Ok(())
105    }
106
107    fn collect_item(&mut self, item: &'tcx Item<'tcx>) -> Result {
108        let owner_id = item.owner_id;
109
110        let mut attrs = self.parse_attrs_and_report_dups(owner_id.def_id)?;
111        self.collect_ignore_and_trusted(&mut attrs, owner_id.def_id);
112        self.collect_infer_opts(&mut attrs, owner_id.def_id);
113        DetachedSpecsCollector::collect(self, &mut attrs)?;
114
115        match &item.kind {
116            ItemKind::Fn { .. } => {
117                self.collect_fn_spec(owner_id, attrs)?;
118            }
119            ItemKind::Struct(_, _, variant) => {
120                self.collect_struct_def(owner_id, attrs, variant)?;
121            }
122            ItemKind::Union(_, _, variant) => {
123                // currently no refinements on unions
124                tracked_span_assert_eq!(attrs.items().is_empty(), true);
125                self.collect_struct_def(owner_id, attrs, variant)?;
126            }
127            ItemKind::Enum(_, _, enum_def) => {
128                self.collect_enum_def(owner_id, attrs, enum_def)?;
129            }
130            ItemKind::Mod(..) => self.collect_mod(owner_id, attrs)?,
131            ItemKind::TyAlias(..) => self.collect_type_alias(owner_id, attrs)?,
132            ItemKind::Impl(..) => self.collect_impl(owner_id, attrs)?,
133            ItemKind::Trait(..) => self.collect_trait(owner_id, attrs)?,
134            ItemKind::Const(.., body_id) => {
135                // The flux-rs macro puts defs as an outer attribute on a `const _: () = { }`. We
136                // consider these defs to be defined in the parent of the const.
137                self.specs
138                    .flux_items_by_parent
139                    .entry(self.tcx.hir_get_parent_item(item.hir_id()))
140                    .or_default()
141                    .extend(attrs.items());
142
143                if attrs.extern_spec() {
144                    return ExternSpecCollector::collect(self, *body_id);
145                }
146
147                self.collect_constant(owner_id, attrs)?;
148            }
149            _ => {}
150        }
151        hir::intravisit::walk_item(self, item);
152        Ok(())
153    }
154
155    fn collect_trait_item(&mut self, trait_item: &'tcx rustc_hir::TraitItem<'tcx>) -> Result {
156        let owner_id = trait_item.owner_id;
157
158        let mut attrs = self.parse_attrs_and_report_dups(owner_id.def_id)?;
159        self.collect_ignore_and_trusted(&mut attrs, owner_id.def_id);
160        self.collect_infer_opts(&mut attrs, owner_id.def_id);
161        if let rustc_hir::TraitItemKind::Fn(_, _) = trait_item.kind {
162            self.collect_fn_spec(owner_id, attrs)?;
163        }
164        hir::intravisit::walk_trait_item(self, trait_item);
165        Ok(())
166    }
167
168    fn collect_impl_item(&mut self, impl_item: &'tcx rustc_hir::ImplItem<'tcx>) -> Result {
169        let owner_id = impl_item.owner_id;
170
171        let mut attrs = self.parse_attrs_and_report_dups(owner_id.def_id)?;
172        self.collect_ignore_and_trusted(&mut attrs, owner_id.def_id);
173        self.collect_infer_opts(&mut attrs, owner_id.def_id);
174
175        if let ImplItemKind::Fn(..) = &impl_item.kind {
176            self.collect_fn_spec(owner_id, attrs)?;
177        }
178        hir::intravisit::walk_impl_item(self, impl_item);
179        Ok(())
180    }
181
182    fn collect_mod(&mut self, module_id: OwnerId, mut attrs: FluxAttrs) -> Result {
183        self.specs
184            .flux_items_by_parent
185            .entry(module_id)
186            .or_default()
187            .extend(attrs.items());
188        Ok(())
189    }
190
191    fn collect_trait(&mut self, owner_id: OwnerId, mut attrs: FluxAttrs) -> Result {
192        let generics = attrs.generics();
193        let assoc_refinements = attrs.trait_assoc_refts();
194
195        self.specs
196            .traits
197            .insert(owner_id, surface::Trait { generics, assoc_refinements });
198
199        Ok(())
200    }
201
202    fn collect_impl(&mut self, owner_id: OwnerId, mut attrs: FluxAttrs) -> Result {
203        let generics = attrs.generics();
204        let assoc_refinements = attrs.impl_assoc_refts();
205
206        self.specs
207            .impls
208            .insert(owner_id, surface::Impl { generics, assoc_refinements });
209
210        Ok(())
211    }
212
213    fn collect_type_alias(&mut self, owner_id: OwnerId, mut attrs: FluxAttrs) -> Result {
214        self.specs
215            .ty_aliases
216            .insert(owner_id, attrs.ty_alias().map(|z| *z));
217        Ok(())
218    }
219
220    fn collect_struct_def(
221        &mut self,
222        owner_id: OwnerId,
223        mut attrs: FluxAttrs,
224        data: &VariantData,
225    ) -> Result<&mut surface::StructDef> {
226        let opaque = attrs.opaque();
227        let refined_by = attrs.refined_by();
228        let generics = attrs.generics();
229
230        let fields = data
231            .fields()
232            .iter()
233            .take(data.fields().len())
234            .map(|field| self.parse_field_spec(field, opaque))
235            .try_collect_exhaust()?;
236
237        let invariants = attrs.invariants();
238
239        Ok(self
240            .specs
241            .structs
242            .entry(owner_id)
243            .or_insert(surface::StructDef { generics, refined_by, fields, opaque, invariants }))
244    }
245
246    fn parse_constant_spec(&mut self, owner_id: OwnerId, mut attrs: FluxAttrs) -> Result {
247        if let Some(constant) = attrs.constant() {
248            self.specs.constants.insert(owner_id, constant);
249        }
250        Ok(())
251    }
252
253    fn parse_field_spec(
254        &mut self,
255        field: &rustc_hir::FieldDef,
256        opaque: bool,
257    ) -> Result<Option<surface::Ty>> {
258        let mut attrs = self.parse_attrs_and_report_dups(field.def_id)?;
259        let field_attr = attrs.field();
260
261        // We warn if a struct marked as opaque has a refined type annotation. We allow unrefined
262        // annotations, because the `flux!` macro unconditionally adds a `#[flux_tool::field(..)]`
263        // annotation, even if the struct is opaque.
264        if opaque
265            && let Some(ty) = field_attr.as_ref()
266            && ty.is_refined()
267        {
268            return Err(self.errors.emit(errors::AttrOnOpaque::new(ty.span, field)));
269        }
270        Ok(field_attr)
271    }
272
273    fn collect_enum_def(
274        &mut self,
275        owner_id: OwnerId,
276        mut attrs: FluxAttrs,
277        enum_def: &EnumDef,
278    ) -> Result<&mut surface::EnumDef> {
279        let generics = attrs.generics();
280        let refined_by = attrs.refined_by();
281        let reflected = attrs.reflected();
282
283        if refined_by.is_some() && reflected {
284            let span = self.tcx.def_span(owner_id.to_def_id());
285            return Err(self
286                .errors
287                .emit(errors::ReflectedEnumWithRefinedBy::new(span)));
288        }
289
290        let variants = enum_def
291            .variants
292            .iter()
293            .take(enum_def.variants.len())
294            .map(|variant| self.collect_variant(variant, refined_by.is_some()))
295            .try_collect_exhaust()?;
296
297        let invariants = attrs.invariants();
298
299        Ok(self
300            .specs
301            .enums
302            .entry(owner_id)
303            .or_insert(surface::EnumDef { generics, refined_by, variants, invariants, reflected }))
304    }
305
306    fn collect_variant(
307        &mut self,
308        hir_variant: &rustc_hir::Variant,
309        has_refined_by: bool,
310    ) -> Result<Option<surface::VariantDef>> {
311        let mut attrs = self.parse_attrs_and_report_dups(hir_variant.def_id)?;
312
313        let variant = attrs.variant();
314
315        if variant.is_none() && has_refined_by {
316            return Err(self
317                .errors
318                .emit(errors::MissingVariant::new(hir_variant.span)));
319        }
320
321        Ok(variant)
322    }
323
324    fn collect_constant(&mut self, owner_id: OwnerId, attrs: FluxAttrs) -> Result {
325        self.parse_constant_spec(owner_id, attrs)
326    }
327
328    fn collect_fn_spec(
329        &mut self,
330        owner_id: OwnerId,
331        mut attrs: FluxAttrs,
332    ) -> Result<&mut surface::FnSpec> {
333        let fn_sig = attrs.fn_sig();
334
335        if let Some(fn_sig) = &fn_sig
336            && let Some(ident) = fn_sig.ident
337            && let Some(item_ident) = self.tcx.opt_item_ident(owner_id.to_def_id())
338            && ident != item_ident
339        {
340            return Err(self.errors.emit(errors::MismatchedSpecName::new(
341                self.tcx,
342                ident,
343                owner_id.to_def_id(),
344            )));
345        };
346
347        if attrs.should_fail() {
348            self.specs.should_fail.insert(owner_id.def_id);
349        }
350
351        let qual_names: Option<surface::QualNames> = attrs.qual_names();
352
353        let reveal_names: Option<surface::RevealNames> = attrs.reveal_names();
354
355        let trusted = matches!(attrs.trusted(), Some(Trusted::Yes));
356
357        Ok(self
358            .specs
359            .fn_sigs
360            .entry(owner_id)
361            .or_insert(surface::FnSpec { fn_sig, qual_names, reveal_names, trusted }))
362    }
363
364    fn parse_attrs_and_report_dups(&mut self, def_id: LocalDefId) -> Result<FluxAttrs> {
365        let attrs = self.parse_flux_attrs(def_id)?;
366        self.report_dups(&attrs)?;
367        Ok(attrs)
368    }
369
370    fn parse_flux_attrs(&mut self, def_id: LocalDefId) -> Result<FluxAttrs> {
371        let def_kind = self.tcx.def_kind(def_id);
372        let hir_id = self.tcx.local_def_id_to_hir_id(def_id);
373        let attrs = self.tcx.hir_attrs(hir_id);
374        let attrs: Vec<_> = attrs
375            .iter()
376            .filter_map(|attr| {
377                if let Attribute::Unparsed(attr_item) = &attr {
378                    match &attr_item.path.segments[..] {
379                        [first, ..] => {
380                            let ident = first.as_str();
381                            if ident == "flux" || ident == "flux_tool" {
382                                Some(attr_item)
383                            } else {
384                                None
385                            }
386                        }
387                        _ => None,
388                    }
389                } else {
390                    None
391                }
392            })
393            .map(|attr_item| self.parse_flux_attr(attr_item, def_kind))
394            .try_collect_exhaust()?;
395
396        Ok(FluxAttrs::new(attrs))
397    }
398
399    fn parse_flux_attr(
400        &mut self,
401        attr_item: &hir::AttrItem,
402        def_kind: DefKind,
403    ) -> Result<FluxAttr> {
404        let invalid_attr_err = |this: &Self| {
405            this.errors
406                .emit(errors::InvalidAttr { span: attr_item_span(attr_item) })
407        };
408
409        let [_, segment] = &attr_item.path.segments[..] else { return Err(invalid_attr_err(self)) };
410
411        let kind = match (segment.as_str(), &attr_item.args) {
412            ("alias", hir::AttrArgs::Delimited(dargs)) => {
413                self.parse(dargs, ParseSess::parse_type_alias, |t| {
414                    FluxAttrKind::TypeAlias(Box::new(t))
415                })?
416            }
417            ("sig" | "spec", hir::AttrArgs::Delimited(dargs)) => {
418                self.parse(dargs, ParseSess::parse_fn_sig, FluxAttrKind::FnSig)?
419            }
420            ("assoc" | "reft", hir::AttrArgs::Delimited(dargs)) => {
421                match def_kind {
422                    DefKind::Trait => {
423                        self.parse(
424                            dargs,
425                            ParseSess::parse_trait_assoc_reft,
426                            FluxAttrKind::TraitAssocReft,
427                        )?
428                    }
429                    DefKind::Impl { .. } => {
430                        self.parse(
431                            dargs,
432                            ParseSess::parse_impl_assoc_reft,
433                            FluxAttrKind::ImplAssocReft,
434                        )?
435                    }
436                    _ => return Err(invalid_attr_err(self)),
437                }
438            }
439            ("qualifiers", hir::AttrArgs::Delimited(dargs)) => {
440                self.parse(dargs, ParseSess::parse_qual_names, FluxAttrKind::QualNames)?
441            }
442            ("reveal", hir::AttrArgs::Delimited(dargs)) => {
443                self.parse(dargs, ParseSess::parse_reveal_names, FluxAttrKind::RevealNames)?
444            }
445            ("defs", hir::AttrArgs::Delimited(dargs)) => {
446                self.parse(dargs, ParseSess::parse_flux_item, FluxAttrKind::Items)?
447            }
448            ("refined_by", hir::AttrArgs::Delimited(dargs)) => {
449                self.parse(dargs, ParseSess::parse_refined_by, FluxAttrKind::RefinedBy)?
450            }
451            ("field", hir::AttrArgs::Delimited(dargs)) => {
452                self.parse(dargs, ParseSess::parse_type, FluxAttrKind::Field)?
453            }
454            ("variant", hir::AttrArgs::Delimited(dargs)) => {
455                self.parse(dargs, ParseSess::parse_variant, FluxAttrKind::Variant)?
456            }
457            ("invariant", hir::AttrArgs::Delimited(dargs)) => {
458                self.parse(dargs, ParseSess::parse_expr, FluxAttrKind::Invariant)?
459            }
460            ("constant", hir::AttrArgs::Delimited(dargs)) => {
461                self.parse(dargs, ParseSess::parse_constant_info, FluxAttrKind::Constant)?
462            }
463            ("opts", hir::AttrArgs::Delimited(..)) => {
464                let opts = AttrMap::parse(attr_item)
465                    .emit(&self.errors)?
466                    .try_into_infer_opts()
467                    .emit(&self.errors)?;
468                FluxAttrKind::InferOpts(opts)
469            }
470            ("ignore", hir::AttrArgs::Delimited(dargs)) => {
471                self.parse(dargs, ParseSess::parse_yes_or_no_with_reason, |b| {
472                    FluxAttrKind::Ignore(b.into())
473                })?
474            }
475            ("ignore", hir::AttrArgs::Empty) => FluxAttrKind::Ignore(Ignored::Yes),
476            ("trusted", hir::AttrArgs::Delimited(dargs)) => {
477                self.parse(dargs, ParseSess::parse_yes_or_no_with_reason, |b| {
478                    FluxAttrKind::Trusted(b.into())
479                })?
480            }
481            ("trusted", hir::AttrArgs::Empty) => FluxAttrKind::Trusted(Trusted::Yes),
482            ("trusted_impl", hir::AttrArgs::Delimited(dargs)) => {
483                self.parse(dargs, ParseSess::parse_yes_or_no_with_reason, |b| {
484                    FluxAttrKind::TrustedImpl(b.into())
485                })?
486            }
487            ("trusted_impl", hir::AttrArgs::Empty) => FluxAttrKind::TrustedImpl(Trusted::Yes),
488            ("opaque", hir::AttrArgs::Empty) => FluxAttrKind::Opaque,
489            ("reflect", hir::AttrArgs::Empty) => FluxAttrKind::Reflect,
490            ("extern_spec", hir::AttrArgs::Empty) => FluxAttrKind::ExternSpec,
491            ("should_fail", hir::AttrArgs::Empty) => FluxAttrKind::ShouldFail,
492            ("specs", hir::AttrArgs::Delimited(dargs)) => {
493                self.parse(dargs, ParseSess::parse_detached_specs, FluxAttrKind::DetachedSpecs)?
494            }
495            _ => return Err(invalid_attr_err(self)),
496        };
497        if config::annots() {
498            self.stats.add(self.tcx, segment.as_str(), &attr_item.args);
499        }
500        Ok(FluxAttr { kind, span: attr_item_span(attr_item) })
501    }
502
503    fn parse<T>(
504        &mut self,
505        dargs: &rustc_ast::DelimArgs,
506        parser: impl FnOnce(&mut ParseSess, &TokenStream, Span) -> ParseResult<T>,
507        ctor: impl FnOnce(T) -> FluxAttrKind,
508    ) -> Result<FluxAttrKind> {
509        let entire = dargs.dspan.entire().with_ctxt(SyntaxContext::root());
510        parser(&mut self.parse_sess, &dargs.tokens, entire)
511            .map(ctor)
512            .map_err(errors::SyntaxErr::from)
513            .emit(&self.errors)
514    }
515
516    fn report_dups(&mut self, attrs: &FluxAttrs) -> Result {
517        let mut err = None;
518        for (name, dups) in attrs.dups() {
519            for attr in dups {
520                if attr.allow_dups() {
521                    continue;
522                }
523                err.collect(
524                    self.errors
525                        .emit(errors::DuplicatedAttr { span: attr.span, name }),
526                );
527            }
528        }
529        err.into_result()
530    }
531
532    fn collect_ignore_and_trusted(&mut self, attrs: &mut FluxAttrs, def_id: LocalDefId) {
533        if let Some(ignored) = attrs.ignore() {
534            self.specs.ignores.insert(def_id, ignored);
535        }
536        if let Some(trusted) = attrs.trusted() {
537            self.specs.trusted.insert(def_id, trusted);
538        }
539        if let Some(trusted_impl) = attrs.trusted_impl() {
540            self.specs.trusted_impl.insert(def_id, trusted_impl);
541        }
542    }
543
544    fn collect_infer_opts(&mut self, attrs: &mut FluxAttrs, def_id: LocalDefId) {
545        if let Some(infer_opts) = attrs.infer_opts() {
546            self.specs.infer_opts.insert(def_id, infer_opts);
547        }
548    }
549}
550
551#[derive(Debug)]
552struct FluxAttrs {
553    map: HashMap<&'static str, Vec<FluxAttr>>,
554}
555
556#[derive(Debug)]
557struct FluxAttr {
558    kind: FluxAttrKind,
559    span: Span,
560}
561
562#[derive(Debug)]
563enum FluxAttrKind {
564    Trusted(Trusted),
565    TrustedImpl(Trusted),
566    Opaque,
567    Reflect,
568    FnSig(surface::FnSig),
569    TraitAssocReft(Vec<surface::TraitAssocReft>),
570    ImplAssocReft(Vec<surface::ImplAssocReft>),
571    RefinedBy(surface::RefineParams),
572    Generics(surface::Generics),
573    QualNames(surface::QualNames),
574    RevealNames(surface::RevealNames),
575    Items(Vec<surface::FluxItem>),
576    TypeAlias(Box<surface::TyAlias>),
577    Field(surface::Ty),
578    Constant(surface::ConstantInfo),
579    Variant(surface::VariantDef),
580    InferOpts(config::PartialInferOpts),
581    Invariant(surface::Expr),
582    Ignore(Ignored),
583    ShouldFail,
584    ExternSpec,
585    /// See `detachXX.rs`
586    DetachedSpecs(surface::DetachedSpecs),
587}
588
589macro_rules! read_flag {
590    ($self:expr, $kind:ident) => {{ $self.map.get(attr_name!($kind)).is_some() }};
591}
592
593macro_rules! read_attrs {
594    ($self:expr, $kind:ident) => {
595        $self
596            .map
597            .remove(attr_name!($kind))
598            .unwrap_or_else(|| vec![])
599            .into_iter()
600            .filter_map(|attr| if let FluxAttrKind::$kind(v) = attr.kind { Some(v) } else { None })
601            .collect::<Vec<_>>()
602    };
603}
604
605macro_rules! read_attr {
606    ($self:expr, $kind:ident) => {
607        read_attrs!($self, $kind).pop()
608    };
609}
610
611impl FluxAttr {
612    pub fn allow_dups(&self) -> bool {
613        matches!(
614            &self.kind,
615            FluxAttrKind::Invariant(..)
616                | FluxAttrKind::TraitAssocReft(..)
617                | FluxAttrKind::ImplAssocReft(..)
618        )
619    }
620}
621
622impl FluxAttrs {
623    fn new(attrs: Vec<FluxAttr>) -> Self {
624        FluxAttrs { map: attrs.into_iter().into_group_map_by(|attr| attr.kind.name()) }
625    }
626
627    fn dups(&self) -> impl Iterator<Item = (&'static str, &[FluxAttr])> {
628        self.map
629            .iter()
630            .filter(|(_, attrs)| attrs.len() > 1)
631            .map(|(name, attrs)| (*name, &attrs[1..]))
632    }
633
634    fn trusted(&mut self) -> Option<Trusted> {
635        read_attr!(self, Trusted)
636    }
637
638    fn trusted_impl(&mut self) -> Option<Trusted> {
639        read_attr!(self, TrustedImpl)
640    }
641
642    fn ignore(&mut self) -> Option<Ignored> {
643        read_attr!(self, Ignore)
644    }
645
646    fn opaque(&self) -> bool {
647        read_flag!(self, Opaque)
648    }
649
650    fn reflected(&self) -> bool {
651        read_flag!(self, Reflect)
652    }
653
654    fn items(&mut self) -> Vec<surface::FluxItem> {
655        read_attrs!(self, Items).into_iter().flatten().collect()
656    }
657
658    fn fn_sig(&mut self) -> Option<surface::FnSig> {
659        read_attr!(self, FnSig)
660    }
661
662    fn qual_names(&mut self) -> Option<surface::QualNames> {
663        read_attr!(self, QualNames)
664    }
665
666    fn reveal_names(&mut self) -> Option<surface::RevealNames> {
667        read_attr!(self, RevealNames)
668    }
669
670    fn ty_alias(&mut self) -> Option<Box<surface::TyAlias>> {
671        read_attr!(self, TypeAlias)
672    }
673
674    fn refined_by(&mut self) -> Option<surface::RefineParams> {
675        read_attr!(self, RefinedBy)
676    }
677
678    fn generics(&mut self) -> Option<surface::Generics> {
679        read_attr!(self, Generics)
680    }
681
682    fn trait_assoc_refts(&mut self) -> Vec<surface::TraitAssocReft> {
683        read_attrs!(self, TraitAssocReft)
684            .into_iter()
685            .flatten()
686            .collect()
687    }
688
689    fn impl_assoc_refts(&mut self) -> Vec<surface::ImplAssocReft> {
690        read_attrs!(self, ImplAssocReft)
691            .into_iter()
692            .flatten()
693            .collect()
694    }
695
696    fn field(&mut self) -> Option<surface::Ty> {
697        read_attr!(self, Field)
698    }
699
700    fn constant(&mut self) -> Option<surface::ConstantInfo> {
701        read_attr!(self, Constant)
702    }
703
704    fn variant(&mut self) -> Option<surface::VariantDef> {
705        read_attr!(self, Variant)
706    }
707
708    fn infer_opts(&mut self) -> Option<config::PartialInferOpts> {
709        read_attr!(self, InferOpts)
710    }
711
712    fn invariants(&mut self) -> Vec<surface::Expr> {
713        read_attrs!(self, Invariant)
714    }
715
716    fn extern_spec(&self) -> bool {
717        read_flag!(self, ExternSpec)
718    }
719
720    fn should_fail(&self) -> bool {
721        read_flag!(self, ShouldFail)
722    }
723
724    fn detached_specs(&mut self) -> Option<surface::DetachedSpecs> {
725        read_attr!(self, DetachedSpecs)
726    }
727}
728
729impl FluxAttrKind {
730    fn name(&self) -> &'static str {
731        match self {
732            FluxAttrKind::Trusted(_) => attr_name!(Trusted),
733            FluxAttrKind::TrustedImpl(_) => attr_name!(TrustedImpl),
734            FluxAttrKind::Opaque => attr_name!(Opaque),
735            FluxAttrKind::Reflect => attr_name!(Reflect),
736            FluxAttrKind::FnSig(_) => attr_name!(FnSig),
737            FluxAttrKind::TraitAssocReft(_) => attr_name!(TraitAssocReft),
738            FluxAttrKind::ImplAssocReft(_) => attr_name!(ImplAssocReft),
739            FluxAttrKind::RefinedBy(_) => attr_name!(RefinedBy),
740            FluxAttrKind::Generics(_) => attr_name!(Generics),
741            FluxAttrKind::Items(_) => attr_name!(Items),
742            FluxAttrKind::QualNames(_) => attr_name!(QualNames),
743            FluxAttrKind::RevealNames(_) => attr_name!(RevealNames),
744            FluxAttrKind::Field(_) => attr_name!(Field),
745            FluxAttrKind::Constant(_) => attr_name!(Constant),
746            FluxAttrKind::Variant(_) => attr_name!(Variant),
747            FluxAttrKind::TypeAlias(_) => attr_name!(TypeAlias),
748            FluxAttrKind::InferOpts(_) => attr_name!(InferOpts),
749            FluxAttrKind::Ignore(_) => attr_name!(Ignore),
750            FluxAttrKind::Invariant(_) => attr_name!(Invariant),
751            FluxAttrKind::ShouldFail => attr_name!(ShouldFail),
752            FluxAttrKind::ExternSpec => attr_name!(ExternSpec),
753            FluxAttrKind::DetachedSpecs(_) => attr_name!(DetachedSpecs),
754        }
755    }
756}
757
758#[derive(Debug)]
759struct AttrMapValue {
760    setting: Symbol,
761    span: Span,
762}
763
764#[derive(Debug)]
765struct AttrMap {
766    map: HashMap<String, AttrMapValue>,
767}
768
769macro_rules! try_read_setting {
770    ($self:expr, $setting:ident, $type:ident, $cfg:expr) => {{
771        let val =
772            if let Some(AttrMapValue { setting, span }) = $self.map.remove(stringify!($setting)) {
773                let parse_result = setting.as_str().parse::<$type>();
774                if let Ok(val) = parse_result {
775                    Some(val)
776                } else {
777                    return Err(errors::AttrMapErr {
778                        span,
779                        message: format!(
780                            "incorrect type in value for setting `{}`, expected {}",
781                            stringify!($setting),
782                            stringify!($type)
783                        ),
784                    });
785                }
786            } else {
787                None
788            };
789        $cfg.$setting = val;
790    }};
791}
792
793type AttrMapErr<T = ()> = std::result::Result<T, errors::AttrMapErr>;
794
795impl AttrMap {
796    fn parse(attr_item: &hir::AttrItem) -> AttrMapErr<Self> {
797        let mut map = Self { map: HashMap::new() };
798        let err = || {
799            Err(errors::AttrMapErr {
800                span: attr_item_span(attr_item),
801                message: "bad syntax".to_string(),
802            })
803        };
804        let hir::AttrArgs::Delimited(d) = &attr_item.args else { return err() };
805        let Some(items) = MetaItemKind::list_from_tokens(d.tokens.clone()) else { return err() };
806        for item in items {
807            map.parse_entry(&item)?;
808        }
809        Ok(map)
810    }
811
812    fn parse_entry(&mut self, nested_item: &MetaItemInner) -> AttrMapErr {
813        match nested_item {
814            MetaItemInner::MetaItem(item) => {
815                let name = item.name().map(|sym| sym.to_ident_string());
816                let span = item.span;
817                if let Some(name) = name {
818                    if self.map.contains_key(&name) {
819                        return Err(errors::AttrMapErr {
820                            span,
821                            message: format!("duplicated key `{name}`"),
822                        });
823                    }
824
825                    // TODO: support types of values other than strings
826                    let value = item.name_value_literal().ok_or_else(|| {
827                        errors::AttrMapErr { span, message: "unsupported value".to_string() }
828                    })?;
829
830                    let setting = AttrMapValue { setting: value.symbol, span: item.span };
831                    self.map.insert(name, setting);
832                    return Ok(());
833                }
834                Err(errors::AttrMapErr { span, message: "bad setting name".to_string() })
835            }
836            MetaItemInner::Lit(_) => {
837                Err(errors::AttrMapErr {
838                    span: nested_item.span(),
839                    message: "unsupported item".to_string(),
840                })
841            }
842        }
843    }
844
845    fn try_into_infer_opts(&mut self) -> AttrMapErr<PartialInferOpts> {
846        let mut infer_opts = PartialInferOpts::default();
847        try_read_setting!(self, allow_uninterpreted_cast, bool, infer_opts);
848        try_read_setting!(self, check_overflow, OverflowMode, infer_opts);
849        try_read_setting!(self, scrape_quals, bool, infer_opts);
850        try_read_setting!(self, solver, SmtSolver, infer_opts);
851
852        if let Some((name, setting)) = self.map.iter().next() {
853            return Err(errors::AttrMapErr {
854                span: setting.span,
855                message: format!("invalid crate cfg keyword `{name}`"),
856            });
857        }
858
859        Ok(infer_opts)
860    }
861}
862
863fn attr_item_span(attr_item: &hir::AttrItem) -> Span {
864    attr_args_span(&attr_item.args)
865        .map_or(attr_item.path.span, |args_span| attr_item.path.span.to(args_span))
866}
867
868fn attr_args_span(attr_args: &hir::AttrArgs) -> Option<Span> {
869    match attr_args {
870        hir::AttrArgs::Empty => None,
871        hir::AttrArgs::Delimited(args) => Some(args.dspan.entire()),
872        hir::AttrArgs::Eq { eq_span, expr } => Some(eq_span.to(expr.span)),
873    }
874}
875
876mod errors {
877    use flux_errors::E0999;
878    use flux_macros::Diagnostic;
879    use flux_syntax::surface::ExprPath;
880    use itertools::Itertools;
881    use rustc_errors::{Diag, DiagCtxtHandle, Diagnostic, Level};
882    use rustc_hir::def_id::DefId;
883    use rustc_middle::ty::TyCtxt;
884    use rustc_span::{ErrorGuaranteed, Span, Symbol, symbol::Ident};
885
886    #[derive(Diagnostic)]
887    #[diag(driver_duplicated_attr, code = E0999)]
888    pub(super) struct DuplicatedAttr {
889        #[primary_span]
890        pub span: Span,
891        pub name: &'static str,
892    }
893
894    #[derive(Diagnostic)]
895    #[diag(driver_invalid_attr, code = E0999)]
896    pub(super) struct InvalidAttr {
897        #[primary_span]
898        pub span: Span,
899    }
900
901    #[derive(Diagnostic)]
902    #[diag(driver_invalid_attr_map, code = E0999)]
903    pub(super) struct AttrMapErr {
904        #[primary_span]
905        pub span: Span,
906        pub message: String,
907    }
908
909    #[derive(Diagnostic)]
910    #[diag(driver_unresolved_specification, code = E0999)]
911    pub(super) struct UnresolvedSpecification {
912        #[primary_span]
913        pub span: Span,
914        pub ident: Ident,
915        pub thing: String,
916    }
917
918    impl UnresolvedSpecification {
919        pub(super) fn new(path: &ExprPath, thing: &str) -> Self {
920            let span = path.span;
921            let ident = path
922                .segments
923                .last()
924                .map_or_else(|| Ident::with_dummy_span(Symbol::intern("")), |seg| seg.ident);
925            Self { span, ident, thing: thing.to_string() }
926        }
927    }
928
929    #[derive(Diagnostic)]
930    #[diag(driver_multiple_specifications, code = E0999)]
931    pub(super) struct MultipleSpecifications {
932        #[primary_span]
933        pub span: Span,
934        pub name: Symbol,
935    }
936
937    pub(super) struct SyntaxErr(flux_syntax::ParseError);
938
939    impl From<flux_syntax::ParseError> for SyntaxErr {
940        fn from(err: flux_syntax::ParseError) -> Self {
941            SyntaxErr(err)
942        }
943    }
944
945    impl<'sess> Diagnostic<'sess> for SyntaxErr {
946        fn into_diag(
947            self,
948            dcx: DiagCtxtHandle<'sess>,
949            level: Level,
950        ) -> Diag<'sess, ErrorGuaranteed> {
951            use flux_syntax::ParseErrorKind;
952            let mut diag = Diag::new(dcx, level, crate::fluent_generated::driver_syntax_err);
953            diag.code(E0999).span(self.0.span).span_label(
954                self.0.span,
955                match &self.0.kind {
956                    ParseErrorKind::UnexpectedEof => "unexpected end of input".to_string(),
957                    ParseErrorKind::UnexpectedToken { expected } => {
958                        match &expected[..] {
959                            [] => "unexpected token".to_string(),
960                            [a] => format!("unexpected token, expected `{a}`"),
961                            [a, b] => format!("unexpected token, expected `{a}` or `{b}`"),
962                            [prefix @ .., last] => {
963                                format!(
964                                    "unexpected token, expected one of {}, or `{last}`",
965                                    prefix
966                                        .iter()
967                                        .format_with(", ", |it, f| f(&format_args!("`{it}`")))
968                                )
969                            }
970                        }
971                    }
972                    ParseErrorKind::CannotBeChained => "operator cannot be chained".to_string(),
973                    ParseErrorKind::InvalidBinding => {
974                        "identifier must be a mutable reference".to_string()
975                    }
976                    ParseErrorKind::InvalidSort => {
977                        "property parameter sort is inherited from the primitive operator"
978                            .to_string()
979                    }
980                    ParseErrorKind::InvalidDetachedSpec => {
981                        "detached spec requires an identifier name".to_string()
982                    }
983                },
984            );
985            diag
986        }
987    }
988
989    #[derive(Diagnostic)]
990    #[diag(driver_attr_on_opaque, code = E0999)]
991    pub(super) struct AttrOnOpaque {
992        #[primary_span]
993        span: Span,
994        #[label]
995        field_span: Span,
996    }
997
998    impl AttrOnOpaque {
999        pub(super) fn new(span: Span, field: &rustc_hir::FieldDef) -> Self {
1000            let field_span = field.ident.span;
1001            Self { span, field_span }
1002        }
1003    }
1004
1005    #[derive(Diagnostic)]
1006    #[diag(driver_reflected_enum_with_refined_by, code = E0999)]
1007    pub(super) struct ReflectedEnumWithRefinedBy {
1008        #[primary_span]
1009        #[label]
1010        span: Span,
1011    }
1012    impl ReflectedEnumWithRefinedBy {
1013        pub(super) fn new(span: Span) -> Self {
1014            Self { span }
1015        }
1016    }
1017
1018    #[derive(Diagnostic)]
1019    #[diag(driver_missing_variant, code = E0999)]
1020    #[note]
1021    pub(super) struct MissingVariant {
1022        #[primary_span]
1023        #[label]
1024        span: Span,
1025    }
1026
1027    impl MissingVariant {
1028        pub(super) fn new(span: Span) -> Self {
1029            Self { span }
1030        }
1031    }
1032
1033    #[derive(Diagnostic)]
1034    #[diag(driver_mismatched_spec_name, code = E0999)]
1035    pub(super) struct MismatchedSpecName {
1036        #[primary_span]
1037        #[label]
1038        span: Span,
1039        #[label(driver_item_def_ident)]
1040        item_ident_span: Span,
1041        item_ident: Ident,
1042        def_descr: &'static str,
1043    }
1044
1045    impl MismatchedSpecName {
1046        pub(super) fn new(tcx: TyCtxt, ident: Ident, def_id: DefId) -> Self {
1047            let def_descr = tcx.def_descr(def_id);
1048            let item_ident = tcx.opt_item_ident(def_id).unwrap();
1049            Self { span: ident.span, item_ident_span: item_ident.span, item_ident, def_descr }
1050        }
1051    }
1052}