1pub mod visit;
2use std::{borrow::Cow, fmt, ops::Range};
3
4pub use rustc_ast::{
5 Mutability,
6 token::{Lit, LitKind},
7};
8pub use rustc_span::{Span, symbol::Ident};
9use rustc_span::{Symbol, symbol::sym};
10
11use crate::surface::visit::Visitor;
12
13#[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)]
16pub struct NodeId(pub(super) usize);
17
18impl NodeId {
19 pub fn as_usize(&self) -> usize {
20 self.0
21 }
22}
23
24#[derive(Debug)]
25pub struct SortDecl {
26 pub name: Ident,
27}
28
29#[derive(Debug)]
30pub enum FluxItem {
31 Qualifier(Qualifier),
32 FuncDef(SpecFunc),
33 SortDecl(SortDecl),
34 PrimOpProp(PrimOpProp),
35}
36
37impl FluxItem {
38 pub fn name(&self) -> Ident {
39 match self {
40 FluxItem::Qualifier(qualifier) => qualifier.name,
41 FluxItem::FuncDef(spec_func) => spec_func.name,
42 FluxItem::SortDecl(sort_decl) => sort_decl.name,
43 FluxItem::PrimOpProp(primop_prop) => primop_prop.name,
44 }
45 }
46}
47
48#[derive(Debug)]
49pub struct Qualifier {
50 pub name: Ident,
51 pub params: RefineParams,
52 pub expr: Expr,
53 pub span: Span,
54 pub global: bool,
55}
56
57#[derive(Debug)]
60pub struct SpecFunc {
61 pub name: Ident,
62 pub sort_vars: Vec<Ident>,
63 pub params: RefineParams,
64 pub output: Sort,
65 pub body: Option<Expr>,
67 pub hide: bool,
71}
72
73#[derive(Debug)]
75pub struct PrimOpProp {
76 pub name: Ident,
78 pub op: BinOp,
80 pub params: RefineParams,
83 pub body: Expr,
85 pub span: Span,
86}
87
88#[derive(Debug)]
89pub struct Generics {
90 pub params: Vec<GenericParam>,
91 pub predicates: Option<Vec<WhereBoundPredicate>>,
92 pub span: Span,
93}
94
95#[derive(Debug)]
96pub struct GenericParam {
97 pub name: Ident,
98 pub node_id: NodeId,
99}
100
101#[derive(Debug)]
102pub struct TyAlias {
103 pub ident: Ident,
104 pub generics: Generics,
105 pub params: RefineParams,
106 pub index: Option<RefineParam>,
107 pub ty: Ty,
108 pub node_id: NodeId,
109 pub span: Span,
110}
111
112#[derive(Debug)]
113pub struct DetachedSpecs {
114 pub items: Vec<Item>,
115}
116
117#[derive(Debug)]
118pub struct DetachedTraitImpl {
119 pub trait_: ExprPath,
120 pub items: Vec<Item<FnSpec>>,
121 pub refts: Vec<ImplAssocReft>,
122 pub span: Span,
123}
124
125#[derive(Debug)]
126pub struct DetachedTrait {
127 pub items: Vec<Item<FnSpec>>,
128 pub refts: Vec<TraitAssocReft>,
129}
130
131#[derive(Debug)]
132pub struct DetachedInherentImpl {
133 pub items: Vec<Item<FnSpec>>,
134 pub span: Span,
135}
136
137impl DetachedInherentImpl {
138 pub fn extend(&mut self, other: DetachedInherentImpl) {
139 self.items.extend(other.items);
140 }
141}
142
143#[derive(Debug)]
144pub struct Item<K = ItemKind> {
145 pub path: ExprPath,
146 pub kind: K,
147}
148
149impl Item<ItemKind> {
150 pub fn span(&self) -> Span {
151 match &self.kind {
152 ItemKind::InherentImpl(impl_) => impl_.span,
153 ItemKind::TraitImpl(trait_impl) => trait_impl.span,
154 _ => self.path.span,
155 }
156 }
157}
158
159#[derive(Debug)]
160pub enum ItemKind {
161 FnSig(FnSpec),
162 Mod(DetachedSpecs),
163 Struct(StructDef),
164 Enum(EnumDef),
165 InherentImpl(DetachedInherentImpl),
166 TraitImpl(DetachedTraitImpl),
167 Trait(DetachedTrait),
168}
169
170#[derive(Debug)]
171pub struct ConstantInfo {
172 pub expr: Option<Expr>,
173}
174
175#[derive(Debug)]
176pub struct StructDef {
177 pub generics: Option<Generics>,
178 pub refined_by: Option<RefineParams>,
179 pub fields: Vec<Option<Ty>>,
180 pub opaque: bool,
181 pub invariants: Vec<Expr>,
182}
183
184impl StructDef {
185 pub fn needs_resolving(&self) -> bool {
187 self.fields.iter().any(Option::is_some)
188 }
189
190 pub fn is_nontrivial(&self) -> bool {
192 self.refined_by.is_some()
193 || !self.invariants.is_empty()
194 || self.opaque
195 || self.fields.iter().any(Option::is_some)
196 }
197}
198
199#[derive(Debug)]
200pub struct EnumDef {
201 pub generics: Option<Generics>,
202 pub refined_by: Option<RefineParams>,
203 pub variants: Vec<Option<VariantDef>>,
204 pub invariants: Vec<Expr>,
205 pub reflected: bool,
206}
207
208impl EnumDef {
209 pub fn needs_resolving(&self) -> bool {
211 self.variants.iter().any(Option::is_some)
212 }
213
214 pub fn is_nontrivial(&self) -> bool {
215 self.refined_by.is_some()
216 || !self.invariants.is_empty()
217 || self.reflected
218 || self.variants.iter().any(Option::is_some)
219 }
220}
221
222#[derive(Debug)]
223pub struct VariantDef {
224 pub ident: Option<Ident>,
225 pub fields: Vec<Ty>,
226 pub ret: Option<VariantRet>,
227 pub node_id: NodeId,
228 pub span: Span,
229}
230
231#[derive(Debug)]
232pub struct VariantRet {
233 pub path: Path,
234 pub indices: Indices,
237}
238
239pub type RefineParams = Vec<RefineParam>;
240
241#[derive(Debug, Default)]
242pub struct QualNames {
243 pub names: Vec<Ident>,
244}
245
246#[derive(Debug, Default)]
247pub struct RevealNames {
248 pub names: Vec<Ident>,
249}
250
251#[derive(Debug)]
252pub struct RefineParam {
253 pub ident: Ident,
254 pub sort: Sort,
255 pub mode: Option<ParamMode>,
256 pub span: Span,
257 pub node_id: NodeId,
258}
259
260#[derive(Clone, Copy, Debug, PartialEq, Eq)]
261pub enum ParamMode {
262 Horn,
263 Hindley,
264}
265
266#[derive(Debug)]
267pub enum Sort {
268 Base(BaseSort),
270 Func { inputs: Vec<BaseSort>, output: BaseSort },
273 Infer,
275}
276
277#[derive(Debug)]
278pub enum BaseSort {
279 BitVec(u32),
281 SortOf(Box<Ty>, Path),
282 Path(SortPath),
283}
284
285#[derive(Debug)]
287pub struct SortPath {
288 pub segments: Vec<Ident>,
290 pub args: Vec<BaseSort>,
292 pub node_id: NodeId,
293}
294
295#[derive(Debug)]
296pub struct Impl {
297 pub generics: Option<Generics>,
298 pub assoc_refinements: Vec<ImplAssocReft>,
299}
300
301impl Impl {
302 pub fn is_nontrivial(&self) -> bool {
303 self.generics.is_some() || !self.assoc_refinements.is_empty()
304 }
305}
306
307#[derive(Debug)]
308pub struct ImplAssocReft {
309 pub name: Ident,
310 pub params: RefineParams,
311 pub output: BaseSort,
312 pub body: Expr,
313 pub span: Span,
314}
315
316#[derive(Debug)]
317pub struct Trait {
318 pub generics: Option<Generics>,
319 pub assoc_refinements: Vec<TraitAssocReft>,
320}
321
322impl Trait {
323 pub fn is_nontrivial(&self) -> bool {
324 self.generics.is_some() || !self.assoc_refinements.is_empty()
325 }
326}
327#[derive(Debug)]
328pub struct TraitAssocReft {
329 pub name: Ident,
330 pub params: RefineParams,
331 pub output: BaseSort,
332 pub body: Option<Expr>,
333 pub span: Span,
334 pub final_: bool,
335}
336
337#[derive(Debug)]
338pub struct FnSpec {
339 pub fn_sig: Option<FnSig>,
340 pub qual_names: Option<QualNames>,
341 pub reveal_names: Option<RevealNames>,
342 pub trusted: bool,
343}
344
345#[derive(Debug)]
346pub struct FnSig {
347 pub asyncness: Async,
348 pub ident: Option<Ident>,
349 pub generics: Generics,
350 pub params: RefineParams,
351 pub requires: Vec<Requires>,
353 pub inputs: Vec<FnInput>,
355 pub output: FnOutput,
356 pub span: Span,
358 pub node_id: NodeId,
359}
360
361#[derive(Debug)]
362pub struct Requires {
363 pub params: RefineParams,
365 pub pred: Expr,
366}
367
368#[derive(Debug)]
369pub struct FnOutput {
370 pub returns: FnRetTy,
372 pub ensures: Vec<Ensures>,
374 pub node_id: NodeId,
375}
376
377#[derive(Debug)]
378pub enum Ensures {
379 Type(Ident, Ty, NodeId),
381 Pred(Expr),
383}
384
385#[derive(Debug)]
386pub enum FnRetTy {
387 Default(Span),
388 Ty(Box<Ty>),
389}
390
391#[derive(Debug, Copy, Clone)]
392pub enum Async {
393 Yes { node_id: NodeId, span: Span },
394 No,
395}
396
397#[derive(Debug)]
398pub struct WhereBoundPredicate {
399 pub span: Span,
400 pub bounded_ty: Ty,
401 pub bounds: GenericBounds,
402}
403
404pub type GenericBounds = Vec<TraitRef>;
405
406#[derive(Debug)]
407pub struct TraitRef {
408 pub path: Path,
409 pub node_id: NodeId,
410}
411
412impl TraitRef {
413 fn is_fn_trait_name(name: Symbol) -> bool {
414 name == sym::FnOnce || name == sym::FnMut || name == sym::Fn
415 }
416
417 pub fn as_fn_trait_ref(&self) -> Option<(&GenericArg, &GenericArg)> {
418 if let [segment] = self.path.segments.as_slice()
419 && Self::is_fn_trait_name(segment.ident.name)
420 && let [in_arg, out_arg] = segment.args.as_slice()
421 {
422 return Some((in_arg, out_arg));
423 }
424 None
425 }
426}
427
428#[derive(Debug)]
429pub enum FnInput {
430 Constr(Ident, Path, Expr, NodeId),
432 StrgRef(Ident, Ty, NodeId),
434 Ty(Option<Ident>, Ty, NodeId),
437}
438
439#[derive(Debug)]
440pub struct Ty {
441 pub kind: TyKind,
442 pub node_id: NodeId,
443 pub span: Span,
444}
445
446#[derive(Debug)]
447pub enum TyKind {
448 Base(BaseTy),
450 Indexed {
452 bty: BaseTy,
453 indices: Indices,
454 },
455 Exists {
457 bind: Ident,
458 bty: BaseTy,
459 pred: Expr,
460 },
461 GeneralExists {
462 params: RefineParams,
463 ty: Box<Ty>,
464 pred: Option<Expr>,
465 },
466 Ref(Mutability, Box<Ty>),
468 Constr(Expr, Box<Ty>),
470 Tuple(Vec<Ty>),
471 Array(Box<Ty>, ConstArg),
472 ImplTrait(NodeId, GenericBounds),
474 Hole,
475}
476
477impl Ty {
478 pub fn is_refined(&self) -> bool {
479 struct IsRefinedVisitor {
480 is_refined: bool,
481 }
482 let mut vis = IsRefinedVisitor { is_refined: false };
483 impl visit::Visitor for IsRefinedVisitor {
484 fn visit_ty(&mut self, ty: &Ty) {
485 match &ty.kind {
486 TyKind::Tuple(_)
487 | TyKind::Ref(..)
488 | TyKind::Array(..)
489 | TyKind::ImplTrait(..)
490 | TyKind::Hole
491 | TyKind::Base(_) => {
492 visit::walk_ty(self, ty);
493 }
494 TyKind::Indexed { .. }
495 | TyKind::Exists { .. }
496 | TyKind::GeneralExists { .. }
497 | TyKind::Constr(..) => {
498 self.is_refined = true;
499 }
500 }
501 }
502 }
503 vis.visit_ty(self);
504 vis.is_refined
505 }
506
507 pub fn is_potential_const_arg(&self) -> Option<&Path> {
508 if let TyKind::Base(bty) = &self.kind
509 && let BaseTyKind::Path(None, path) = &bty.kind
510 && let [segment] = &path.segments[..]
511 && segment.args.is_empty()
512 {
513 Some(path)
514 } else {
515 None
516 }
517 }
518}
519#[derive(Debug)]
520pub struct BaseTy {
521 pub kind: BaseTyKind,
522 pub span: Span,
523}
524
525#[derive(Debug)]
526pub enum BaseTyKind {
527 Path(Option<Box<Ty>>, Path),
528 Slice(Box<Ty>),
529}
530
531#[derive(PartialEq, Eq, Clone, Debug, Copy)]
532pub struct ConstArg {
533 pub kind: ConstArgKind,
534 pub span: Span,
535}
536
537#[derive(PartialEq, Eq, Clone, Debug, Copy)]
538pub enum ConstArgKind {
539 Lit(usize),
540 Infer,
541}
542
543#[derive(Debug)]
544pub struct Indices {
545 pub indices: Vec<RefineArg>,
546 pub span: Span,
547}
548
549#[derive(Debug)]
550pub enum RefineArg {
551 Bind(Ident, BindKind, Span, NodeId),
553 Expr(Expr),
554 Abs(RefineParams, Expr, Span, NodeId),
555}
556
557#[derive(Debug, Clone, Copy)]
558pub enum BindKind {
559 At,
560 Pound,
561}
562
563#[derive(Debug)]
564pub enum Attr {
565 Trusted,
567 Hide,
569 Reft,
571 Invariant(Expr),
573 RefinedBy(RefineParams),
575}
576
577pub struct Attrs(pub Vec<Attr>);
578
579impl Attrs {
580 pub fn is_reft(&self) -> bool {
581 self.0.iter().any(|attr| matches!(attr, Attr::Reft))
582 }
583
584 pub fn is_trusted(&self) -> bool {
585 self.0.iter().any(|attr| matches!(attr, Attr::Trusted))
586 }
587
588 pub fn refined_by(&mut self) -> Option<RefineParams> {
589 let pos = self
590 .0
591 .iter()
592 .position(|x| matches!(x, Attr::RefinedBy(_)))?;
593 if let Attr::RefinedBy(params) = self.0.remove(pos) { Some(params) } else { None }
594 }
595
596 pub fn invariant(&mut self) -> Option<Expr> {
597 let pos = self
598 .0
599 .iter()
600 .position(|x| matches!(x, Attr::Invariant(_)))?;
601 if let Attr::Invariant(exp) = self.0.remove(pos) { Some(exp) } else { None }
602 }
603}
604
605#[derive(Debug)]
606pub struct Path {
607 pub segments: Vec<PathSegment>,
608 pub refine: Vec<RefineArg>,
609 pub node_id: NodeId,
610 pub span: Span,
611}
612
613impl Path {
614 pub fn last(&self) -> &PathSegment {
615 self.segments
616 .last()
617 .expect("path must have at least one segment")
618 }
619}
620
621#[derive(Debug)]
622pub struct PathSegment {
623 pub ident: Ident,
624 pub args: Vec<GenericArg>,
625 pub node_id: NodeId,
626}
627
628#[derive(Debug)]
629pub struct GenericArg {
630 pub kind: GenericArgKind,
631 pub node_id: NodeId,
632}
633
634#[derive(Debug)]
635pub enum GenericArgKind {
636 Type(Ty),
637 Constraint(Ident, Ty),
638}
639
640#[derive(Debug)]
641pub struct FieldExpr {
642 pub ident: Ident,
643 pub expr: Expr,
644 pub span: Span,
645 pub node_id: NodeId,
646}
647
648#[derive(Debug)]
649pub struct Spread {
650 pub expr: Expr,
651 pub span: Span,
652 pub node_id: NodeId,
653}
654
655#[derive(Debug)]
656pub enum ConstructorArg {
657 FieldExpr(FieldExpr),
658 Spread(Spread),
659}
660
661#[derive(Debug)]
662pub struct Expr {
663 pub kind: ExprKind,
664 pub node_id: NodeId,
665 pub span: Span,
666}
667
668#[derive(Debug)]
669pub enum QuantKind {
670 Forall,
671 Exists,
672}
673
674#[derive(Debug)]
675pub enum ExprKind {
676 Path(ExprPath),
677 Dot(Box<Expr>, Ident),
678 Literal(Lit),
679 BinaryOp(BinOp, Box<[Expr; 2]>),
680 UnaryOp(UnOp, Box<Expr>),
681 Call(Box<Expr>, Vec<Expr>),
682 PrimUIF(BinOp),
684 AssocReft(Box<Ty>, Path, Ident),
686 IfThenElse(Box<[Expr; 3]>),
687 Constructor(Option<ExprPath>, Vec<ConstructorArg>),
688 BoundedQuant(QuantKind, RefineParam, Range<usize>, Box<Expr>),
689 Block(Vec<LetDecl>, Box<Expr>),
690}
691
692#[derive(Debug)]
693pub struct LetDecl {
694 pub param: RefineParam,
695 pub init: Expr,
696}
697
698#[derive(Debug, Clone)]
700pub struct ExprPath {
701 pub segments: Vec<ExprPathSegment>,
702 pub node_id: NodeId,
703 pub span: Span,
704}
705
706#[derive(Debug, Clone)]
707pub struct ExprPathSegment {
708 pub ident: Ident,
709 pub node_id: NodeId,
710}
711#[derive(Copy, Clone, Hash, Eq, PartialEq)]
712pub enum BinOp {
713 Iff,
714 Imp,
715 Or,
716 And,
717 Eq,
718 Ne,
719 Gt,
720 Ge,
721 Lt,
722 Le,
723 Add,
724 Sub,
725 Mul,
726 Div,
727 Mod,
728 BitOr,
729 BitXor,
730 BitAnd,
731 BitShl,
732 BitShr,
733}
734
735impl fmt::Debug for BinOp {
736 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
737 match self {
738 BinOp::Iff => write!(f, "<=>"),
739 BinOp::Imp => write!(f, "=>"),
740 BinOp::Or => write!(f, "||"),
741 BinOp::And => write!(f, "&&"),
742 BinOp::Eq => write!(f, "=="),
743 BinOp::Ne => write!(f, "!="),
744 BinOp::Lt => write!(f, "<"),
745 BinOp::Le => write!(f, "<="),
746 BinOp::Gt => write!(f, ">"),
747 BinOp::Ge => write!(f, ">="),
748 BinOp::Add => write!(f, "+"),
749 BinOp::Sub => write!(f, "-"),
750 BinOp::Mod => write!(f, "mod"),
751 BinOp::Mul => write!(f, "*"),
752 BinOp::Div => write!(f, "/"),
753 BinOp::BitOr => write!(f, "|"),
754 BinOp::BitXor => write!(f, "^"),
755 BinOp::BitAnd => write!(f, "&"),
756 BinOp::BitShl => write!(f, "<<"),
757 BinOp::BitShr => write!(f, ">>"),
758 }
759 }
760}
761
762impl rustc_errors::IntoDiagArg for BinOp {
763 fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
764 rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
765 }
766}
767
768#[derive(Copy, Clone)]
769pub enum UnOp {
770 Not,
771 Neg,
772}
773
774impl fmt::Debug for UnOp {
775 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
776 match self {
777 Self::Not => write!(f, "!"),
778 Self::Neg => write!(f, "-"),
779 }
780 }
781}
782
783impl BindKind {
784 pub fn token_str(&self) -> &'static str {
785 match self {
786 BindKind::At => "@",
787 BindKind::Pound => "#",
788 }
789 }
790}
791
792pub struct Punctuated<T, P> {
794 inner: Vec<(T, P)>,
795 last: Option<Box<T>>,
796}
797
798impl<T, P> From<Vec<(T, P)>> for Punctuated<T, P> {
799 fn from(inner: Vec<(T, P)>) -> Self {
800 Self { inner, last: None }
801 }
802}
803
804impl<T, P> Punctuated<T, P> {
805 pub fn len(&self) -> usize {
806 self.inner.len() + self.last.is_some() as usize
807 }
808
809 pub fn is_empty(&self) -> bool {
812 self.inner.len() == 0 && self.last.is_none()
813 }
814
815 pub fn push_value(&mut self, value: T) {
823 assert!(
824 self.empty_or_trailing(),
825 "Punctuated::push_value: cannot push value if Punctuated is missing trailing punctuation",
826 );
827
828 self.last = Some(Box::new(value));
829 }
830
831 pub fn empty_or_trailing(&self) -> bool {
836 self.last.is_none()
837 }
838
839 pub fn trailing_punct(&self) -> bool {
842 self.last.is_none() && !self.is_empty()
843 }
844
845 pub fn into_values(self) -> Vec<T> {
846 let mut v: Vec<T> = self.inner.into_iter().map(|(v, _)| v).collect();
847 if let Some(last) = self.last {
848 v.push(*last);
849 }
850 v
851 }
852}