Skip to main content

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