cranelift_isle/
ast.rs

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

cranelift_isle/
ast.rs
