flux_driver/collector/
mod.rs

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