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