1pub mod visit;
2
3use std::{borrow::Cow, fmt, ops::Range};
4
5use flux_config::PartialInferOpts;
6pub use rustc_ast::{
7 Mutability,
8 token::{Lit, LitKind},
9};
10use rustc_hash::FxHashSet;
11pub use rustc_span::{Span, symbol::Ident};
12use rustc_span::{Symbol, symbol::sym};
13
14use crate::surface::visit::Visitor;
15
16#[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)]
19pub struct NodeId(pub(super) usize);
20
21impl NodeId {
22 pub fn as_usize(&self) -> usize {
23 self.0
24 }
25}
26
27#[derive(Debug)]
28pub struct SortDecl {
29 pub name: Ident,
30 pub sort_vars: Vec<Ident>,
31}
32
33#[derive(Debug)]
34pub enum FluxItem {
35 Qualifier(Qualifier),
36 FuncDef(SpecFunc),
37 SortDecl(SortDecl),
38 PrimOpProp(PrimOpProp),
39 Use(UseTree),
40}
41
42impl FluxItem {
43 pub fn name(&self) -> Option<Ident> {
44 match self {
45 FluxItem::Qualifier(qualifier) => Some(qualifier.name),
46 FluxItem::FuncDef(spec_func) => Some(spec_func.name),
47 FluxItem::SortDecl(sort_decl) => Some(sort_decl.name),
48 FluxItem::PrimOpProp(primop_prop) => Some(primop_prop.name),
49 FluxItem::Use(_) => None,
50 }
51 }
52}
53
54#[derive(Debug)]
55pub struct UseTree {
56 pub prefix: ExprPath,
57 pub kind: UseTreeKind,
58}
59
60#[derive(Debug)]
61pub enum UseTreeKind {
62 Simple,
64 Nested(Vec<UseTree>),
66}
67
68#[derive(Debug)]
69pub struct Qualifier {
70 pub name: Ident,
71 pub params: RefineParams,
72 pub wildcards: Vec<bool>,
73 pub expr: Expr,
74 pub span: Span,
75 pub kind: QualifierKind,
76}
77
78#[derive(Debug)]
79pub enum QualifierKind {
80 Global,
81 Local,
82 Hint,
83}
84
85#[derive(Debug)]
88pub struct SpecFunc {
89 pub name: Ident,
90 pub sort_vars: Vec<Ident>,
91 pub params: RefineParams,
92 pub output: Sort,
93 pub body: Option<Expr>,
95 pub hide: bool,
99}
100
101#[derive(Debug)]
103pub struct PrimOpProp {
104 pub name: Ident,
106 pub op: BinOp,
108 pub params: RefineParams,
111 pub body: Expr,
113 pub span: Span,
114}
115
116#[derive(Debug)]
117pub struct Generics {
118 pub params: Vec<GenericParam>,
119 pub predicates: Option<Vec<WhereBoundPredicate>>,
120 pub span: Span,
121}
122
123#[derive(Debug)]
124pub struct GenericParam {
125 pub name: Ident,
126 pub node_id: NodeId,
127}
128
129#[derive(Debug)]
130pub struct TyAlias {
131 pub ident: Ident,
132 pub generics: Generics,
133 pub params: RefineParams,
134 pub index: Option<RefineParam>,
135 pub ty: Ty,
136 pub node_id: NodeId,
137 pub span: Span,
138}
139
140pub struct Item {
141 pub attrs: Vec<Attr>,
142 pub kind: ItemKind,
143 pub node_id: NodeId,
144}
145
146pub enum ItemKind {
147 Fn(Option<FnSig>),
148 Struct(StructDef),
149 Enum(EnumDef),
150 Trait(Trait),
151 Impl(Impl),
152 Const(ConstantInfo),
153 TyAlias(Box<TyAlias>),
154 Static(StaticInfo),
155 Mod,
158}
159
160pub struct TraitItemFn {
161 pub attrs: Vec<Attr>,
162 pub sig: Option<FnSig>,
163 pub node_id: NodeId,
164}
165
166pub struct ImplItemFn {
167 pub attrs: Vec<Attr>,
168 pub sig: Option<FnSig>,
169 pub node_id: NodeId,
170}
171
172#[derive(Debug)]
173pub struct DetachedSpecs {
174 pub items: Vec<DetachedItem>,
175}
176
177#[derive(Debug)]
178pub struct DetachedTraitImpl {
179 pub trait_: ExprPath,
180 pub items: Vec<DetachedItem<FnSig>>,
181 pub refts: Vec<ImplAssocReft>,
182 pub span: Span,
183}
184
185#[derive(Debug, Default)]
186pub struct DetachedTrait {
187 pub items: Vec<DetachedItem<FnSig>>,
188 pub refts: Vec<TraitAssocReft>,
189}
190
191#[derive(Debug)]
192pub struct DetachedInherentImpl {
193 pub items: Vec<DetachedItem<FnSig>>,
194 pub span: Span,
195}
196
197impl DetachedInherentImpl {
198 pub fn extend(&mut self, other: DetachedInherentImpl) {
199 self.items.extend(other.items);
200 }
201}
202
203#[derive(Debug)]
204pub struct DetachedItem<K = DetachedItemKind> {
205 pub attrs: Vec<Attr>,
206 pub path: ExprPath,
207 pub kind: K,
208 pub node_id: NodeId,
209}
210
211impl<K> DetachedItem<K> {
212 pub fn map_kind<R>(self, f: impl FnOnce(K) -> R) -> DetachedItem<R> {
213 DetachedItem {
214 attrs: self.attrs,
215 path: self.path,
216 kind: f(self.kind),
217 node_id: self.node_id,
218 }
219 }
220}
221
222impl DetachedItem<DetachedItemKind> {
223 pub fn span(&self) -> Span {
224 match &self.kind {
225 DetachedItemKind::InherentImpl(impl_) => impl_.span,
226 DetachedItemKind::TraitImpl(trait_impl) => trait_impl.span,
227 _ => self.path.span,
228 }
229 }
230}
231
232#[derive(Debug)]
233pub enum DetachedItemKind {
234 FnSig(FnSig),
235 Mod(DetachedSpecs),
236 Struct(StructDef),
237 Enum(EnumDef),
238 InherentImpl(DetachedInherentImpl),
239 TraitImpl(DetachedTraitImpl),
240 Trait(DetachedTrait),
241 Static(StaticInfo),
242}
243
244#[derive(Debug)]
245pub struct ConstantInfo {
246 pub expr: Option<Expr>,
247}
248
249#[derive(Debug)]
250pub struct StaticInfo {
251 pub ty: Ty,
252}
253
254#[derive(Debug)]
255pub struct StructDef {
256 pub generics: Option<Generics>,
257 pub refined_by: Option<RefineParams>,
258 pub fields: Vec<Option<Ty>>,
259 pub opaque: bool,
260 pub invariants: Vec<Expr>,
261}
262
263#[derive(Debug)]
264pub struct EnumDef {
265 pub generics: Option<Generics>,
266 pub refined_by: Option<RefineParams>,
267 pub variants: Vec<Option<VariantDef>>,
268 pub invariants: Vec<Expr>,
269 pub reflected: bool,
270}
271
272#[derive(Debug)]
273pub struct VariantDef {
274 pub ident: Option<Ident>,
275 pub fields: Vec<Ty>,
276 pub ret: Option<VariantRet>,
277 pub node_id: NodeId,
278 pub span: Span,
279}
280
281#[derive(Debug)]
282pub struct VariantRet {
283 pub path: Path,
284 pub indices: Indices,
287}
288
289pub type RefineParams = Vec<RefineParam>;
290
291#[derive(Debug)]
292pub struct RefineParam {
293 pub ident: Ident,
294 pub sort: Sort,
295 pub mode: Option<ParamMode>,
296 pub span: Span,
297 pub node_id: NodeId,
298}
299
300#[derive(Clone, Copy, Debug, PartialEq, Eq)]
301pub enum ParamMode {
302 Horn,
303 Hindley,
304}
305
306#[derive(Debug)]
307pub enum Sort {
308 Base(BaseSort),
310 Func { inputs: Vec<BaseSort>, output: BaseSort },
313 Infer,
315}
316
317#[derive(Debug)]
318pub enum BaseSort {
319 BitVec(u32),
321 SortOf(Box<Ty>, Path),
322 Path(SortPath),
323 Tuple(Vec<BaseSort>),
325}
326
327#[derive(Debug)]
329pub struct SortPath {
330 pub segments: Vec<Ident>,
332 pub args: Vec<BaseSort>,
334 pub node_id: NodeId,
335}
336
337#[derive(Debug)]
338pub struct Impl {
339 pub generics: Option<Generics>,
340 pub assoc_refinements: Vec<ImplAssocReft>,
341}
342
343#[derive(Debug)]
344pub struct ImplAssocReft {
345 pub name: Ident,
346 pub params: RefineParams,
347 pub output: BaseSort,
348 pub body: Expr,
349 pub span: Span,
350}
351
352#[derive(Debug)]
353pub struct Trait {
354 pub generics: Option<Generics>,
355 pub assoc_refinements: Vec<TraitAssocReft>,
356}
357
358#[derive(Debug)]
359pub struct TraitAssocReft {
360 pub name: Ident,
361 pub params: RefineParams,
362 pub output: BaseSort,
363 pub body: Option<Expr>,
364 pub span: Span,
365 pub final_: bool,
366}
367
368#[derive(Debug)]
369pub struct FnSig {
370 pub asyncness: Async,
371 pub ident: Option<Ident>,
372 pub generics: Generics,
373 pub params: RefineParams,
374 pub requires: Vec<Requires>,
376 pub inputs: Vec<FnInput>,
378 pub output: FnOutput,
379 pub span: Span,
381 pub node_id: NodeId,
382 pub no_panic: Option<Expr>,
383}
384
385#[derive(Debug)]
386pub struct Requires {
387 pub params: RefineParams,
389 pub pred: Expr,
390}
391
392#[derive(Debug)]
393pub struct FnOutput {
394 pub returns: FnRetTy,
396 pub ensures: Vec<Ensures>,
398 pub node_id: NodeId,
399}
400
401#[derive(Debug)]
402pub enum Ensures {
403 Type(Ident, Ty, NodeId),
405 Pred(Expr),
407}
408
409#[derive(Debug)]
410pub enum FnRetTy {
411 Default(Span),
412 Ty(Box<Ty>),
413}
414
415#[derive(Debug, Copy, Clone)]
416pub enum Async {
417 Yes { node_id: NodeId, span: Span },
418 No,
419}
420
421#[derive(Debug)]
422pub struct WhereBoundPredicate {
423 pub span: Span,
424 pub bounded_ty: Ty,
425 pub bounds: GenericBounds,
426}
427
428pub type GenericBounds = Vec<TraitRef>;
429
430#[derive(Debug)]
431pub struct TraitRef {
432 pub path: Path,
433 pub node_id: NodeId,
434}
435
436impl TraitRef {
437 fn is_fn_trait_name(name: Symbol) -> bool {
438 name == sym::FnOnce || name == sym::FnMut || name == sym::Fn
439 }
440
441 pub fn as_fn_trait_ref(&self) -> Option<(&GenericArg, &GenericArg)> {
442 if let [segment] = self.path.segments.as_slice()
443 && Self::is_fn_trait_name(segment.ident.name)
444 && let [in_arg, out_arg] = segment.args.as_slice()
445 {
446 return Some((in_arg, out_arg));
447 }
448 None
449 }
450}
451
452#[derive(Debug)]
453pub enum FnInput {
454 Constr(Ident, Path, Expr, NodeId),
456 StrgRef(Ident, Ty, NodeId),
458 Ty(Option<Ident>, Ty, NodeId),
461}
462
463#[derive(Debug)]
464pub struct Ty {
465 pub kind: TyKind,
466 pub node_id: NodeId,
467 pub span: Span,
468}
469
470#[derive(Debug)]
471pub enum TyKind {
472 Base(BaseTy),
474 Indexed {
476 bty: BaseTy,
477 indices: Indices,
478 },
479 Exists {
481 bind: Ident,
482 bty: BaseTy,
483 pred: Expr,
484 },
485 GeneralExists {
486 params: RefineParams,
487 ty: Box<Ty>,
488 pred: Option<Expr>,
489 },
490 Ref(Mutability, Box<Ty>),
492 Constr(Expr, Box<Ty>),
494 Tuple(Vec<Ty>),
495 Array(Box<Ty>, ConstArg),
496 ImplTrait(NodeId, GenericBounds),
498 Hole,
499}
500
501impl Ty {
502 pub fn is_refined(&self) -> bool {
503 struct IsRefinedVisitor {
504 is_refined: bool,
505 }
506 let mut vis = IsRefinedVisitor { is_refined: false };
507 impl visit::Visitor for IsRefinedVisitor {
508 fn visit_ty(&mut self, ty: &Ty) {
509 match &ty.kind {
510 TyKind::Tuple(_)
511 | TyKind::Ref(..)
512 | TyKind::Array(..)
513 | TyKind::ImplTrait(..)
514 | TyKind::Hole
515 | TyKind::Base(_) => {
516 visit::walk_ty(self, ty);
517 }
518 TyKind::Indexed { .. }
519 | TyKind::Exists { .. }
520 | TyKind::GeneralExists { .. }
521 | TyKind::Constr(..) => {
522 self.is_refined = true;
523 }
524 }
525 }
526 }
527 vis.visit_ty(self);
528 vis.is_refined
529 }
530
531 pub fn is_potential_const_arg(&self) -> Option<&Path> {
532 if let TyKind::Base(bty) = &self.kind
533 && let BaseTyKind::Path(None, path) = &bty.kind
534 && let [segment] = &path.segments[..]
535 && segment.args.is_empty()
536 {
537 Some(path)
538 } else {
539 None
540 }
541 }
542}
543#[derive(Debug)]
544pub struct BaseTy {
545 pub kind: BaseTyKind,
546 pub span: Span,
547}
548
549#[derive(Debug)]
550pub enum BaseTyKind {
551 Path(Option<Box<Ty>>, Path),
552 Slice(Box<Ty>),
553 Ptr(Mutability, Box<Ty>),
555}
556
557#[derive(Debug)]
558pub struct ConstArg {
559 pub kind: ConstArgKind,
560 pub span: Span,
561}
562
563#[derive(Debug)]
564pub enum ConstArgKind {
565 Lit(usize),
566 Path(Path),
567 Infer,
568}
569
570#[derive(Debug)]
571pub struct Indices {
572 pub indices: Vec<RefineArg>,
573 pub span: Span,
574}
575
576#[derive(Debug)]
577pub enum RefineArg {
578 Bind(Ident, BindKind, Span, NodeId),
580 Expr(Expr),
581 Abs(RefineParams, Expr, Span, NodeId),
582}
583
584#[derive(Debug, Clone, Copy)]
585pub enum BindKind {
586 At,
587 Pound,
588}
589
590#[derive(Debug, Eq, PartialEq, Copy, Clone)]
592pub enum Trusted {
593 Yes,
594 No,
595}
596
597impl Trusted {
598 pub fn to_bool(self) -> bool {
599 match self {
600 Trusted::Yes => true,
601 Trusted::No => false,
602 }
603 }
604}
605
606impl From<bool> for Trusted {
607 fn from(value: bool) -> Self {
608 if value { Trusted::Yes } else { Trusted::No }
609 }
610}
611
612#[derive(Debug, Eq, PartialEq, Copy, Clone)]
614pub enum Ignored {
615 Yes,
616 No,
617}
618
619impl Ignored {
620 pub fn to_bool(self) -> bool {
621 match self {
622 Ignored::Yes => true,
623 Ignored::No => false,
624 }
625 }
626}
627
628impl From<bool> for Ignored {
629 fn from(value: bool) -> Self {
630 if value { Ignored::Yes } else { Ignored::No }
631 }
632}
633
634#[derive(Debug)]
643pub enum Attr {
644 Trusted(Trusted),
646 TrustedImpl(Trusted),
648 TrustedDerive(Trusted),
650 Ignore(Ignored),
652 ProvenExternally(Span),
654 ShouldFail,
656 Qualifiers(Vec<Ident>),
658 Reveal(Vec<Ident>),
660 InferOpts(PartialInferOpts),
662 NoPanic,
664 AssumeParametric(Vec<Ident>),
666 NoSuggestions,
668}
669
670#[derive(Debug)]
671pub struct Path {
672 pub segments: Vec<PathSegment>,
673 pub refine: Vec<RefineArg>,
674 pub node_id: NodeId,
675 pub span: Span,
676}
677
678impl Path {
679 pub fn last(&self) -> &PathSegment {
680 self.segments
681 .last()
682 .expect("path must have at least one segment")
683 }
684}
685
686#[derive(Debug)]
687pub struct PathSegment {
688 pub ident: Ident,
689 pub args: Vec<GenericArg>,
690 pub node_id: NodeId,
691}
692
693#[derive(Debug)]
694pub struct GenericArg {
695 pub kind: GenericArgKind,
696 pub node_id: NodeId,
697}
698
699#[derive(Debug)]
700pub enum GenericArgKind {
701 Type(Ty),
702 Constraint(Ident, Ty),
703}
704
705#[derive(Debug)]
706pub struct FieldExpr {
707 pub ident: Ident,
708 pub expr: RefineArg,
709 pub span: Span,
710 pub node_id: NodeId,
711}
712
713#[derive(Debug)]
714pub struct Spread {
715 pub expr: Expr,
716 pub span: Span,
717 pub node_id: NodeId,
718}
719
720#[derive(Debug)]
721pub enum ConstructorArg {
722 FieldExpr(FieldExpr),
723 Spread(Spread),
724}
725
726#[derive(Debug)]
727pub struct Expr {
728 pub kind: ExprKind,
729 pub node_id: NodeId,
730 pub span: Span,
731}
732
733#[derive(Debug)]
734pub enum QuantKind {
735 Forall,
736 Exists,
737}
738
739#[derive(Debug)]
740pub enum ExprKind {
741 Path(ExprPath),
742 Dot(Box<Expr>, Ident),
743 Literal(Lit),
744 BinaryOp(BinOp, Box<[Expr; 2]>),
745 UnaryOp(UnOp, Box<Expr>),
746 Call(Box<Expr>, Vec<Expr>),
747 PrimUIF(BinOp),
749 AssocReft(Box<Ty>, Path, Ident),
751 IfThenElse(Box<[Expr; 3]>),
752 Constructor(Option<ExprPath>, Vec<ConstructorArg>),
753 Quant(QuantKind, RefineParam, Option<Range<usize>>, Box<Expr>),
754 Block(Vec<LetDecl>, Box<Expr>),
755 SetLiteral(Vec<Expr>),
757 Tuple(Vec<Expr>),
759}
760
761#[derive(Debug)]
762pub struct LetDecl {
763 pub param: RefineParam,
764 pub init: Expr,
765}
766
767#[derive(Debug, Clone)]
769pub struct ExprPath {
770 pub segments: Vec<ExprPathSegment>,
771 pub node_id: NodeId,
772 pub span: Span,
773}
774
775#[derive(Debug, Clone)]
776pub struct ExprPathSegment {
777 pub ident: Ident,
778 pub node_id: NodeId,
779}
780#[derive(Copy, Clone, Hash, Eq, PartialEq)]
781pub enum BinOp {
782 Iff,
783 Imp,
784 Or,
785 And,
786 Eq,
787 Ne,
788 Gt,
789 Ge,
790 Lt,
791 Le,
792 Add,
793 Sub,
794 Mul,
795 Div,
796 Mod,
797 BitOr,
798 BitXor,
799 BitAnd,
800 BitShl,
801 BitShr,
802}
803
804impl fmt::Debug for BinOp {
805 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
806 match self {
807 BinOp::Iff => write!(f, "<=>"),
808 BinOp::Imp => write!(f, "=>"),
809 BinOp::Or => write!(f, "||"),
810 BinOp::And => write!(f, "&&"),
811 BinOp::Eq => write!(f, "=="),
812 BinOp::Ne => write!(f, "!="),
813 BinOp::Lt => write!(f, "<"),
814 BinOp::Le => write!(f, "<="),
815 BinOp::Gt => write!(f, ">"),
816 BinOp::Ge => write!(f, ">="),
817 BinOp::Add => write!(f, "+"),
818 BinOp::Sub => write!(f, "-"),
819 BinOp::Mod => write!(f, "mod"),
820 BinOp::Mul => write!(f, "*"),
821 BinOp::Div => write!(f, "/"),
822 BinOp::BitOr => write!(f, "|"),
823 BinOp::BitXor => write!(f, "^"),
824 BinOp::BitAnd => write!(f, "&"),
825 BinOp::BitShl => write!(f, "<<"),
826 BinOp::BitShr => write!(f, ">>"),
827 }
828 }
829}
830
831impl rustc_errors::IntoDiagArg for BinOp {
832 fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
833 rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
834 }
835}
836
837#[derive(Copy, Clone)]
838pub enum UnOp {
839 Not,
840 Neg,
841}
842
843impl fmt::Debug for UnOp {
844 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
845 match self {
846 Self::Not => write!(f, "!"),
847 Self::Neg => write!(f, "-"),
848 }
849 }
850}
851
852impl BindKind {
853 pub fn token_str(&self) -> &'static str {
854 match self {
855 BindKind::At => "@",
856 BindKind::Pound => "#",
857 }
858 }
859}
860
861pub struct Punctuated<T, P> {
863 inner: Vec<(T, P)>,
864 last: Option<Box<T>>,
865}
866
867impl<T, P> From<Vec<(T, P)>> for Punctuated<T, P> {
868 fn from(inner: Vec<(T, P)>) -> Self {
869 Self { inner, last: None }
870 }
871}
872
873impl<T, P> Punctuated<T, P> {
874 pub fn len(&self) -> usize {
875 self.inner.len() + self.last.is_some() as usize
876 }
877
878 pub fn is_empty(&self) -> bool {
881 self.inner.len() == 0 && self.last.is_none()
882 }
883
884 pub fn push_value(&mut self, value: T) {
892 assert!(
893 self.empty_or_trailing(),
894 "Punctuated::push_value: cannot push value if Punctuated is missing trailing punctuation",
895 );
896
897 self.last = Some(Box::new(value));
898 }
899
900 pub fn empty_or_trailing(&self) -> bool {
905 self.last.is_none()
906 }
907
908 pub fn trailing_punct(&self) -> bool {
911 self.last.is_none() && !self.is_empty()
912 }
913
914 pub fn into_values(self) -> Vec<T> {
915 let mut v: Vec<T> = self.inner.into_iter().map(|(v, _)| v).collect();
916 if let Some(last) = self.last {
917 v.push(*last);
918 }
919 v
920 }
921}
922
923impl Expr {
924 pub fn free_vars(&self) -> FxHashSet<Ident> {
927 struct FreeVarsVisitor {
928 vars: FxHashSet<Ident>,
929 }
930
931 impl visit::Visitor for FreeVarsVisitor {
932 fn visit_expr(&mut self, expr: &Expr) {
933 match &expr.kind {
934 ExprKind::Path(path) => {
935 if let [segment] = path.segments.as_slice() {
937 self.vars.insert(segment.ident);
938 }
939 }
940 ExprKind::Call(callee, args) => {
941 if !matches!(&callee.kind, ExprKind::Path(_)) {
945 self.visit_expr(callee);
946 }
947 for arg in args {
948 self.visit_expr(arg);
949 }
950 }
951 _ => visit::walk_expr(self, expr),
953 }
954 }
955 }
956
957 let mut visitor = FreeVarsVisitor { vars: FxHashSet::default() };
958 visitor.visit_expr(self);
959 visitor.vars
960 }
961}