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