cranelift_isle/
ast.rs

1//! Abstract syntax tree (AST) created from parsed ISLE.
2
3#![expect(missing_docs, reason = "fields mostly self-describing")]
4
5use crate::lexer::Pos;
6use crate::log;
7
8/// One toplevel form in an ISLE file.
9#[derive(Clone, PartialEq, Eq, Debug)]
10pub 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)]
26pub struct Ident(pub String, pub Pos);
27
28/// Pragmas parsed with the `(pragma <ident>)` syntax.
29#[derive(Clone, PartialEq, Eq, Debug)]
30pub 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)]
36pub 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)]
48pub 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)]
55pub 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)]
63pub 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)]
71pub 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)]
90pub 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)]
135pub 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)]
212pub 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)]
225pub 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)]
238pub 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)]
247pub 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)]
255pub 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)]
263pub struct Form {
264    pub name: Ident,
265    pub signatures: Vec<Signature>,
266    pub pos: Pos,
267}
268
269#[derive(Clone, PartialEq, Eq, Debug)]
270pub 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)]
278pub 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)]
288pub 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)]
297pub 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)]
306pub 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
343impl Pattern {
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.
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
377    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
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
483    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)]
504pub 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
527impl Expr {
528    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.
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)]
564pub 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)]
574pub 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)]
607pub 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}
cranelift_isle/ast.rs

cranelift_isle/
ast.rs
