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 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 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 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 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 for (field, hir_field) in iter::zip(&fields, data.fields()) {
309 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 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 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 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 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 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 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 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 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
1074fn 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}