xref: /wasmtime-44.0.1/cranelift/isle/isle/src/ast.rs (revision 8ec3ff3b)
1 //! Abstract syntax tree (AST) created from parsed ISLE.
2 
3 #![expect(missing_docs, reason = "fields mostly self-describing")]
4 
5 use crate::lexer::Pos;
6 use crate::log;
7 
8 /// One toplevel form in an ISLE file.
9 #[derive(Clone, PartialEq, Eq, Debug)]
10 pub enum Def {
11     Pragma(Pragma),
12     Type(Type),
13     Rule(Rule),
14     Extractor(Extractor),
15     Decl(Decl),
16     Spec(Spec),
17     Model(Model),
18     Form(Form),
19     Instantiation(Instantiation),
20     Extern(Extern),
21     Converter(Converter),
22 }
23 
24 /// An identifier -- a variable, term symbol, or type.
25 #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
26 pub struct Ident(pub String, pub Pos);
27 
28 /// Pragmas parsed with the `(pragma <ident>)` syntax.
29 #[derive(Clone, PartialEq, Eq, Debug)]
30 pub enum Pragma {
31     // currently, no pragmas are defined, but the infrastructure is useful to keep around
32 }
33 
34 /// A declaration of a type.
35 #[derive(Clone, PartialEq, Eq, Debug)]
36 pub struct Type {
37     pub name: Ident,
38     pub is_extern: bool,
39     pub is_nodebug: bool,
40     pub ty: TypeValue,
41     pub pos: Pos,
42 }
43 
44 /// The actual type-value: a primitive or an enum with variants.
45 ///
46 /// TODO: add structs as well?
47 #[derive(Clone, PartialEq, Eq, Debug)]
48 pub enum TypeValue {
49     Primitive(Ident, Pos),
50     Enum(Vec<Variant>, Pos),
51 }
52 
53 /// One variant of an enum type.
54 #[derive(Clone, PartialEq, Eq, Debug)]
55 pub struct Variant {
56     pub name: Ident,
57     pub fields: Vec<Field>,
58     pub pos: Pos,
59 }
60 
61 /// One field of an enum variant.
62 #[derive(Clone, PartialEq, Eq, Debug)]
63 pub struct Field {
64     pub name: Ident,
65     pub ty: Ident,
66     pub pos: Pos,
67 }
68 
69 /// A declaration of a term with its argument and return types.
70 #[derive(Clone, PartialEq, Eq, Debug)]
71 pub struct Decl {
72     pub term: Ident,
73     pub arg_tys: Vec<Ident>,
74     pub ret_ty: Ident,
75     /// Whether this term's constructor is pure.
76     pub pure: bool,
77     /// Whether this term can exist with some multiplicity: an
78     /// extractor or a constructor that matches multiple times, or
79     /// produces multiple values.
80     pub multi: bool,
81     /// Whether this term's constructor can fail to match.
82     pub partial: bool,
83     /// Whether this term is permitted to be recursive.
84     pub rec: bool,
85     pub pos: Pos,
86 }
87 
88 /// An expression used to specify term semantics, similar to SMT-LIB syntax.
89 #[derive(Clone, PartialEq, Eq, Debug)]
90 pub enum SpecExpr {
91     /// An operator that matches a constant integer value.
92     ConstInt {
93         val: i128,
94         pos: Pos,
95     },
96     /// An operator that matches a constant bitvector value.
97     ConstBitVec {
98         val: i128,
99         width: i8,
100         pos: Pos,
101     },
102     /// An operator that matches a constant boolean value.
103     ConstBool {
104         val: bool,
105         pos: Pos,
106     },
107     /// The Unit constant value.
108     ConstUnit {
109         pos: Pos,
110     },
111     // A variable
112     Var {
113         var: Ident,
114         pos: Pos,
115     },
116     /// An application of a type variant or term.
117     Op {
118         op: SpecOp,
119         args: Vec<SpecExpr>,
120         pos: Pos,
121     },
122     /// Pairs, currently used for switch statements.
123     Pair {
124         l: Box<SpecExpr>,
125         r: Box<SpecExpr>,
126     },
127     /// Enums variant values (enums defined by model)
128     Enum {
129         name: Ident,
130     },
131 }
132 
133 /// An operation used to specify term semantics, similar to SMT-LIB syntax.
134 #[derive(Clone, PartialEq, Eq, Debug)]
135 pub enum SpecOp {
136     // Boolean operations
137     Eq,
138     And,
139     Or,
140     Not,
141     Imp,
142 
143     // Integer comparisons
144     Lt,
145     Lte,
146     Gt,
147     Gte,
148 
149     // Bitwise bitvector operations (directly SMT-LIB)
150     BVNot,
151     BVAnd,
152     BVOr,
153     BVXor,
154 
155     // Bitvector arithmetic operations  (directly SMT-LIB)
156     BVNeg,
157     BVAdd,
158     BVSub,
159     BVMul,
160     BVUdiv,
161     BVUrem,
162     BVSdiv,
163     BVSrem,
164     BVShl,
165     BVLshr,
166     BVAshr,
167 
168     // Bitvector comparison operations  (directly SMT-LIB)
169     BVUle,
170     BVUlt,
171     BVUgt,
172     BVUge,
173     BVSlt,
174     BVSle,
175     BVSgt,
176     BVSge,
177 
178     // Bitvector overflow checks (SMT-LIB pending standardization)
179     BVSaddo,
180 
181     // Desugared bitvector arithmetic operations
182     Rotr,
183     Rotl,
184     Extract,
185     ZeroExt,
186     SignExt,
187     Concat,
188 
189     // Custom encodings
190     Subs,
191     Popcnt,
192     Clz,
193     Cls,
194     Rev,
195 
196     // Conversion operations
197     ConvTo,
198     Int2BV,
199     BV2Int,
200     WidthOf,
201 
202     // Control operations
203     If,
204     Switch,
205 
206     LoadEffect,
207     StoreEffect,
208 }
209 
210 /// A specification of the semantics of a term.
211 #[derive(Clone, PartialEq, Eq, Debug)]
212 pub struct Spec {
213     /// The term name (must match a (decl ...))
214     pub term: Ident,
215     /// Argument names
216     pub args: Vec<Ident>,
217     /// Provide statements, which give the semantics of the produces value
218     pub provides: Vec<SpecExpr>,
219     /// Require statements, which express preconditions on the term
220     pub requires: Vec<SpecExpr>,
221 }
222 
223 /// A model of an SMT-LIB type.
224 #[derive(Clone, PartialEq, Eq, Debug)]
225 pub enum ModelType {
226     /// SMT-LIB Int
227     Int,
228     /// SMT-LIB Bool
229     Bool,
230     /// SMT-LIB bitvector, but with a potentially-polymorphic width
231     BitVec(Option<usize>),
232     /// Unit (removed before conversion to SMT-LIB)
233     Unit,
234 }
235 
236 /// A construct's value in SMT-LIB
237 #[derive(Clone, PartialEq, Eq, Debug)]
238 pub enum ModelValue {
239     /// Correspond to ISLE types
240     TypeValue(ModelType),
241     /// Correspond to ISLE enums, identifier is the enum variant name
242     EnumValues(Vec<(Ident, SpecExpr)>),
243 }
244 
245 /// A model of a construct into SMT-LIB (currently, types or enums)
246 #[derive(Clone, PartialEq, Eq, Debug)]
247 pub struct Model {
248     /// The name of the type or enum
249     pub name: Ident,
250     /// The value of the type or enum (potentially multiple values)
251     pub val: ModelValue,
252 }
253 
254 #[derive(Clone, PartialEq, Eq, Debug)]
255 pub struct Signature {
256     pub args: Vec<ModelType>,
257     pub ret: ModelType,
258     pub canonical: ModelType,
259     pub pos: Pos,
260 }
261 
262 #[derive(Clone, PartialEq, Eq, Debug)]
263 pub struct Form {
264     pub name: Ident,
265     pub signatures: Vec<Signature>,
266     pub pos: Pos,
267 }
268 
269 #[derive(Clone, PartialEq, Eq, Debug)]
270 pub struct Instantiation {
271     pub term: Ident,
272     pub form: Option<Ident>,
273     pub signatures: Vec<Signature>,
274     pub pos: Pos,
275 }
276 
277 #[derive(Clone, PartialEq, Eq, Debug)]
278 pub struct Rule {
279     pub pattern: Pattern,
280     pub iflets: Vec<IfLet>,
281     pub expr: Expr,
282     pub pos: Pos,
283     pub prio: Option<i64>,
284     pub name: Option<Ident>,
285 }
286 
287 #[derive(Clone, PartialEq, Eq, Debug)]
288 pub struct IfLet {
289     pub pattern: Pattern,
290     pub expr: Expr,
291     pub pos: Pos,
292 }
293 
294 /// An extractor macro: (A x y) becomes (B x _ y ...). Expanded during
295 /// ast-to-sema pass.
296 #[derive(Clone, PartialEq, Eq, Debug)]
297 pub struct Extractor {
298     pub term: Ident,
299     pub args: Vec<Ident>,
300     pub template: Pattern,
301     pub pos: Pos,
302 }
303 
304 /// A pattern: the left-hand side of a rule.
305 #[derive(Clone, PartialEq, Eq, Debug)]
306 pub enum Pattern {
307     /// A mention of a variable.
308     ///
309     /// Equivalent either to a binding (which can be emulated with
310     /// `BindPattern` with a `Pattern::Wildcard` subpattern), if this
311     /// is the first mention of the variable, in order to capture its
312     /// value; or else a match of the already-captured value. This
313     /// disambiguation happens when we lower `ast` nodes to `sema`
314     /// nodes as we resolve bound variable names.
315     Var { var: Ident, pos: Pos },
316     /// An operator that binds a variable to a subterm and matches the
317     /// subpattern.
318     BindPattern {
319         var: Ident,
320         subpat: Box<Pattern>,
321         pos: Pos,
322     },
323     /// An operator that matches a constant boolean value.
324     ConstBool { val: bool, pos: Pos },
325     /// An operator that matches a constant integer value.
326     ConstInt { val: i128, pos: Pos },
327     /// An operator that matches an external constant value.
328     ConstPrim { val: Ident, pos: Pos },
329     /// An application of a type variant or term.
330     Term {
331         sym: Ident,
332         args: Vec<Pattern>,
333         pos: Pos,
334     },
335     /// An operator that matches anything.
336     Wildcard { pos: Pos },
337     /// N sub-patterns that must all match.
338     And { subpats: Vec<Pattern>, pos: Pos },
339     /// Internal use only: macro argument in a template.
340     MacroArg { index: usize, pos: Pos },
341 }
342 
343 impl Pattern {
root_term(&self) -> Option<&Ident>344     pub fn root_term(&self) -> Option<&Ident> {
345         match self {
346             &Pattern::Term { ref sym, .. } => Some(sym),
347             _ => None,
348         }
349     }
350 
351     /// Call `f` for each of the terms in this pattern.
terms(&self, f: &mut dyn FnMut(Pos, &Ident))352     pub fn terms(&self, f: &mut dyn FnMut(Pos, &Ident)) {
353         match self {
354             Pattern::Term { sym, args, pos } => {
355                 f(*pos, sym);
356                 for arg in args {
357                     arg.terms(f);
358                 }
359             }
360             Pattern::And { subpats, .. } => {
361                 for p in subpats {
362                     p.terms(f);
363                 }
364             }
365             Pattern::BindPattern { subpat, .. } => {
366                 subpat.terms(f);
367             }
368             Pattern::Var { .. }
369             | Pattern::ConstBool { .. }
370             | Pattern::ConstInt { .. }
371             | Pattern::ConstPrim { .. }
372             | Pattern::Wildcard { .. }
373             | Pattern::MacroArg { .. } => {}
374         }
375     }
376 
make_macro_template(&self, macro_args: &[Ident]) -> Pattern377     pub fn make_macro_template(&self, macro_args: &[Ident]) -> Pattern {
378         log!("make_macro_template: {:?} with {:?}", self, macro_args);
379         match self {
380             &Pattern::BindPattern {
381                 ref var,
382                 ref subpat,
383                 pos,
384                 ..
385             } if matches!(&**subpat, &Pattern::Wildcard { .. }) => {
386                 if let Some(i) = macro_args.iter().position(|arg| arg.0 == var.0) {
387                     Pattern::MacroArg { index: i, pos }
388                 } else {
389                     self.clone()
390                 }
391             }
392             &Pattern::BindPattern {
393                 ref var,
394                 ref subpat,
395                 pos,
396             } => Pattern::BindPattern {
397                 var: var.clone(),
398                 subpat: Box::new(subpat.make_macro_template(macro_args)),
399                 pos,
400             },
401             &Pattern::Var { ref var, pos } => {
402                 if let Some(i) = macro_args.iter().position(|arg| arg.0 == var.0) {
403                     Pattern::MacroArg { index: i, pos }
404                 } else {
405                     self.clone()
406                 }
407             }
408             &Pattern::And { ref subpats, pos } => {
409                 let subpats = subpats
410                     .iter()
411                     .map(|subpat| subpat.make_macro_template(macro_args))
412                     .collect::<Vec<_>>();
413                 Pattern::And { subpats, pos }
414             }
415             &Pattern::Term {
416                 ref sym,
417                 ref args,
418                 pos,
419             } => {
420                 let args = args
421                     .iter()
422                     .map(|arg| arg.make_macro_template(macro_args))
423                     .collect::<Vec<_>>();
424                 Pattern::Term {
425                     sym: sym.clone(),
426                     args,
427                     pos,
428                 }
429             }
430 
431             &Pattern::Wildcard { .. }
432             | &Pattern::ConstBool { .. }
433             | &Pattern::ConstInt { .. }
434             | &Pattern::ConstPrim { .. } => self.clone(),
435             &Pattern::MacroArg { .. } => unreachable!(),
436         }
437     }
438 
subst_macro_args(&self, macro_args: &[Pattern]) -> Option<Pattern>439     pub fn subst_macro_args(&self, macro_args: &[Pattern]) -> Option<Pattern> {
440         log!("subst_macro_args: {:?} with {:?}", self, macro_args);
441         match self {
442             &Pattern::BindPattern {
443                 ref var,
444                 ref subpat,
445                 pos,
446             } => Some(Pattern::BindPattern {
447                 var: var.clone(),
448                 subpat: Box::new(subpat.subst_macro_args(macro_args)?),
449                 pos,
450             }),
451             &Pattern::And { ref subpats, pos } => {
452                 let subpats = subpats
453                     .iter()
454                     .map(|subpat| subpat.subst_macro_args(macro_args))
455                     .collect::<Option<Vec<_>>>()?;
456                 Some(Pattern::And { subpats, pos })
457             }
458             &Pattern::Term {
459                 ref sym,
460                 ref args,
461                 pos,
462             } => {
463                 let args = args
464                     .iter()
465                     .map(|arg| arg.subst_macro_args(macro_args))
466                     .collect::<Option<Vec<_>>>()?;
467                 Some(Pattern::Term {
468                     sym: sym.clone(),
469                     args,
470                     pos,
471                 })
472             }
473 
474             &Pattern::Var { .. }
475             | &Pattern::Wildcard { .. }
476             | &Pattern::ConstBool { .. }
477             | &Pattern::ConstInt { .. }
478             | &Pattern::ConstPrim { .. } => Some(self.clone()),
479             &Pattern::MacroArg { index, .. } => macro_args.get(index).cloned(),
480         }
481     }
482 
pos(&self) -> Pos483     pub fn pos(&self) -> Pos {
484         match self {
485             &Pattern::ConstBool { pos, .. }
486             | &Pattern::ConstInt { pos, .. }
487             | &Pattern::ConstPrim { pos, .. }
488             | &Pattern::And { pos, .. }
489             | &Pattern::Term { pos, .. }
490             | &Pattern::BindPattern { pos, .. }
491             | &Pattern::Var { pos, .. }
492             | &Pattern::Wildcard { pos, .. }
493             | &Pattern::MacroArg { pos, .. } => pos,
494         }
495     }
496 }
497 
498 /// An expression: the right-hand side of a rule.
499 ///
500 /// Note that this *almost* looks like a core Lisp or lambda calculus,
501 /// except that there is no abstraction (lambda). This first-order
502 /// limit is what makes it analyzable.
503 #[derive(Clone, PartialEq, Eq, Debug)]
504 pub enum Expr {
505     /// A term: `(sym args...)`.
506     Term {
507         sym: Ident,
508         args: Vec<Expr>,
509         pos: Pos,
510     },
511     /// A variable use.
512     Var { name: Ident, pos: Pos },
513     /// A constant boolean.
514     ConstBool { val: bool, pos: Pos },
515     /// A constant integer.
516     ConstInt { val: i128, pos: Pos },
517     /// A constant of some other primitive type.
518     ConstPrim { val: Ident, pos: Pos },
519     /// The `(let ((var ty val)*) body)` form.
520     Let {
521         defs: Vec<LetDef>,
522         body: Box<Expr>,
523         pos: Pos,
524     },
525 }
526 
527 impl Expr {
pos(&self) -> Pos528     pub fn pos(&self) -> Pos {
529         match self {
530             &Expr::Term { pos, .. }
531             | &Expr::Var { pos, .. }
532             | &Expr::ConstBool { pos, .. }
533             | &Expr::ConstInt { pos, .. }
534             | &Expr::ConstPrim { pos, .. }
535             | &Expr::Let { pos, .. } => pos,
536         }
537     }
538 
539     /// Call `f` for each of the terms in this expression.
terms(&self, f: &mut dyn FnMut(Pos, &Ident))540     pub fn terms(&self, f: &mut dyn FnMut(Pos, &Ident)) {
541         match self {
542             Expr::Term { sym, args, pos } => {
543                 f(*pos, sym);
544                 for arg in args {
545                     arg.terms(f);
546                 }
547             }
548             Expr::Let { defs, body, .. } => {
549                 for def in defs {
550                     def.val.terms(f);
551                 }
552                 body.terms(f);
553             }
554             Expr::Var { .. }
555             | Expr::ConstBool { .. }
556             | Expr::ConstInt { .. }
557             | Expr::ConstPrim { .. } => {}
558         }
559     }
560 }
561 
562 /// One variable locally bound in a `(let ...)` expression.
563 #[derive(Clone, PartialEq, Eq, Debug)]
564 pub struct LetDef {
565     pub var: Ident,
566     pub ty: Ident,
567     pub val: Box<Expr>,
568     pub pos: Pos,
569 }
570 
571 /// An external binding: an extractor or constructor function attached
572 /// to a term.
573 #[derive(Clone, PartialEq, Eq, Debug)]
574 pub enum Extern {
575     /// An external extractor: `(extractor Term rustfunc)` form.
576     Extractor {
577         /// The term to which this external extractor is attached.
578         term: Ident,
579         /// The Rust function name.
580         func: Ident,
581         /// The position of this decl.
582         pos: Pos,
583         /// Infallibility: if an external extractor returns `(T1, T2,
584         /// ...)` rather than `Option<(T1, T2, ...)>`, and hence can
585         /// never fail, it is declared as such and allows for slightly
586         /// better code to be generated.
587         infallible: bool,
588     },
589     /// An external constructor: `(constructor Term rustfunc)` form.
590     Constructor {
591         /// The term to which this external constructor is attached.
592         term: Ident,
593         /// The Rust function name.
594         func: Ident,
595         /// The position of this decl.
596         pos: Pos,
597     },
598     /// An external constant: `(const $IDENT type)` form.
599     Const { name: Ident, ty: Ident, pos: Pos },
600 }
601 
602 /// An implicit converter: the given term, which must have type
603 /// (inner_ty) -> outer_ty, is used either in extractor or constructor
604 /// position as appropriate when a type mismatch with the given pair
605 /// of types would otherwise occur.
606 #[derive(Clone, Debug, PartialEq, Eq)]
607 pub struct Converter {
608     /// The term name.
609     pub term: Ident,
610     /// The "inner type": the type to convert *from*, on the
611     /// right-hand side, or *to*, on the left-hand side. Must match
612     /// the singular argument type of the term.
613     pub inner_ty: Ident,
614     /// The "outer type": the type to convert *to*, on the right-hand
615     /// side, or *from*, on the left-hand side. Must match the ret_ty
616     /// of the term.
617     pub outer_ty: Ident,
618     /// The position of this converter decl.
619     pub pos: Pos,
620 }
621