flux_driver/collector/
mod.rs

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