Repair/RepairCompiler/MCC/IR/SemanticChecker.java

   1 package MCC.IR;
   2
   3 import java.util.*;
   4 import java.math.BigInteger;
   5 import MCC.State;
   6
   7 public class SemanticChecker {
   8
   9     private static final boolean CREATE_MISSING = true;
  10
  11     public State state;
  12
  13     Vector vConstraints;
  14     Vector vRules;
  15
  16     SymbolTableStack sts;
  17
  18     SymbolTable stSets;
  19     SymbolTable stRelations;
  20     SymbolTable stTypes;
  21     SymbolTable stGlobals;
  22
  23     StructureTypeDescriptor dCurrentType;
  24
  25     IRErrorReporter er;
  26
  27     public SemanticChecker () {
  28         dCurrentType = null;
  29         stTypes = null;
  30         er = null;
  31     }
  32
  33     public boolean check(State state, IRErrorReporter er) {
  34
  35         this.state = state;
  36         State.currentState = state;
  37
  38         if (er == null) {
  39             throw new IRException("IRBuilder.build: Received null ErrorReporter");
  40         } else {
  41             this.er = er;
  42         }
  43
  44         if (state.ptStructures == null) {
  45             throw new IRException("IRBuilder.build: Received null ParseNode");
  46         }
  47
  48         state.vConstraints = new Vector();
  49         vConstraints = state.vConstraints;
  50
  51         state.vRules = new Vector();
  52         vRules = state.vRules;
  53
  54         state.stTypes = new SymbolTable();
  55         stTypes = state.stTypes;
  56
  57         state.stSets = new SymbolTable();
  58         stSets = state.stSets;
  59
  60         state.stRelations = new SymbolTable();
  61         stRelations = state.stRelations;
  62
  63         state.stGlobals = new SymbolTable();
  64         stGlobals = state.stGlobals;
  65
  66         sts = new SymbolTableStack();
  67
  68         // add int and bool to the types list
  69         stTypes.add(ReservedTypeDescriptor.BIT);
  70         stTypes.add(ReservedTypeDescriptor.BYTE);
  71         stTypes.add(ReservedTypeDescriptor.SHORT);
  72         stTypes.add(ReservedTypeDescriptor.INT);
  73
  74         stSets.add(new ReservedSetDescriptor("int", ReservedTypeDescriptor.INT));
  75         stSets.add(new ReservedSetDescriptor("token", ReservedTypeDescriptor.INT));
  76
  77         boolean ok = true;
  78
  79         er.setFilename(state.infile + ".struct");
  80         if (!parse_structures(state.ptStructures)) {
  81             ok = false;
  82         }
  83
  84         er.setFilename(state.infile + ".space");
  85         if (!parse_space(state.ptSpace)) {
  86             ok = false;
  87         }
  88
  89         er.setFilename(state.infile + ".constraints");
  90         if (!parse_constraints(state.ptConstraints)) {
  91             ok = false;
  92         }
  93
  94         er.setFilename(state.infile + ".model");
  95         if (!parse_rules(state.ptModel)) {
  96             ok = false;
  97         }
  98
  99         return ok;
 100     }
 101
 102     /********************** HELPER FUNCTIONS ************************/
 103
 104     /**
 105      * special case lookup that returns null if no such type exists
 106      */
 107     private TypeDescriptor lookupType(String typename) {
 108         return lookupType(typename, false);
 109     }
 110
 111     /**
 112      * does a look up in the types symbol table. if the type is
 113      * not found than a missing type descriptor is returned
 114      */
 115     private TypeDescriptor lookupType(String typename, boolean createmissing) {
 116         if (stTypes.get(typename) != null) {
 117             // the type exists, so plug in the descriptor directly
 118             return (TypeDescriptor) stTypes.get(typename);
 119         } else if (createmissing) {
 120             return new MissingTypeDescriptor(typename);
 121         } else {
 122             return null;
 123         }
 124     }
 125
 126     /**
 127      * reserve a name
 128      */
 129     private VarDescriptor reserveName(ParseNode pn) {
 130         assert pn != null;
 131         String varname = pn.getTerminal();
 132         assert varname != null;
 133
 134         /* do semantic check and if valid, add it to symbol table
 135            and add it to the quantifier as well */
 136         if (sts.peek().contains(varname)) {
 137             /* Semantic Error: redefinition */
 138             er.report(pn, "Redefinition of '" + varname + "'");
 139             return null;
 140         } else {
 141             VarDescriptor vd = new VarDescriptor(varname);
 142             sts.peek().add(vd);
 143             return vd;
 144         }
 145     }
 146
 147     /**
 148      * special case lookup that returns null if no such set exists
 149      */
 150     private SetDescriptor lookupSet(String setname) {
 151         return lookupSet(setname, false);
 152     }
 153
 154     /**
 155      * does a look up in the set's symbol table. if the set is
 156      * not found than a missing set descriptor is returned
 157      */
 158     private SetDescriptor lookupSet(String setname, boolean createmissing) {
 159         if (stSets.get(setname) != null) {
 160             // the set exists, so plug in the descriptor directly
 161             return (SetDescriptor) stSets.get(setname);
 162         } else if (createmissing) {
 163             return new MissingSetDescriptor(setname);
 164         } else {
 165             return null;
 166         }
 167     }
 168
 169     /**
 170      * does a look up in the set's symbol table. if the set is
 171      * not found than a missing set descriptor is returned
 172      */
 173     private RelationDescriptor lookupRelation(String relname) {
 174         if (stRelations.get(relname) != null) {
 175             // the relation exists, so plug in the descriptor directly
 176             return (RelationDescriptor) stRelations.get(relname);
 177         } else {
 178             return null;
 179         }
 180     }
 181
 182
 183     private static int count = 0;
 184     private boolean precheck(ParseNode pn, String label) {
 185         if (pn == null) {
 186             er.report(pn, "IE: Expected '" + label + "', got null");
 187             assert false;
 188             return false;
 189         }
 190
 191         if (! pn.getLabel().equals(label)) {
 192             er.report(pn, "IE: Expected '" + label + "', got '" + pn.getLabel() + "'");
 193             assert false;
 194             return false;
 195         }
 196
 197         if (state.verbose >= 2) {
 198             System.err.println("visiting*" + (count++) + ": " + label);
 199         }
 200
 201         return true;
 202     }
 203
 204     /********************* PARSING FUNCTIONS ************************/
 205
 206     private boolean parse_rules(ParseNode pn) {
 207         if (!precheck(pn, "rules")) {
 208             return false;
 209         }
 210
 211         boolean ok = true;
 212         ParseNodeVector rules = pn.getChildren();
 213
 214         for (int i = 0; i < rules.size(); i++) {
 215             ParseNode rule = rules.elementAt(i);
 216             if (!parse_rule(rule)) {
 217                 ok = false;
 218             }
 219         }
 220
 221         /* type check */
 222         Iterator ruleiterator = state.vRules.iterator();
 223
 224         while (ruleiterator.hasNext()) {
 225             Rule rule = (Rule) ruleiterator.next();
 226             Expr guard = rule.getGuardExpr();
 227             final SymbolTable rulest = rule.getSymbolTable();
 228             SemanticAnalyzer sa = new SemanticAnalyzer() {
 229                     public IRErrorReporter getErrorReporter() { return er; }
 230                     public SymbolTable getSymbolTable() { return rulest; }
 231                 };
 232             TypeDescriptor guardtype = guard.typecheck(sa);
 233
 234             if (guardtype == null) {
 235                 ok = false;
 236             } else if (guardtype != ReservedTypeDescriptor.INT) {
 237                 er.report(null, "Type of guard must be 'int' not '" + guardtype.getSymbol() + "'");
 238                 ok = false;
 239             }
 240
 241             if (!rule.getInclusion().typecheck(sa)) {
 242                 ok = false;
 243             }
 244
 245             Iterator quantifiers = rule.quantifiers();
 246
 247             while (quantifiers.hasNext()) {
 248                 Quantifier q = (Quantifier) quantifiers.next();
 249
 250                 if (q instanceof ForQuantifier && !((ForQuantifier)q).typecheck(sa)) {
 251                     ok = false;
 252                 }
 253             }
 254         }
 255
 256         /* do any post checks ?? */
 257
 258         return ok;
 259     }
 260
 261     private boolean parse_rule(ParseNode pn) {
 262         if (!precheck(pn, "rule")) {
 263             return false;
 264         }
 265
 266         boolean ok = true;
 267         Rule rule = new Rule();
 268
 269         /* get rule type */
 270         boolean isstatic = pn.getChild("static") != null;
 271         boolean isdelay = pn.getChild("delay") != null;
 272         rule.setStatic(isstatic);
 273         rule.setDelay(isdelay);
 274
 275         /* set up symbol table for constraint */
 276         assert sts.empty();
 277         sts.push(stGlobals);
 278         sts.push(rule.getSymbolTable());
 279
 280         /* optional quantifiers */
 281         if (pn.getChild("quantifiers") != null) {
 282             ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
 283
 284             for (int i = 0; i < quantifiers.size(); i++) {
 285                 ParseNode qn = quantifiers.elementAt(i);
 286                 Quantifier quantifier = parse_quantifier(qn);
 287
 288                 if (quantifier == null) {
 289                     ok = false;
 290                 } else {
 291                     rule.addQuantifier(quantifier);
 292                 }
 293             }
 294         }
 295
 296         /* get guard expr */
 297         Expr guard = parse_expr(pn.getChild("expr"));
 298
 299         if (guard == null) {
 300             ok = false;
 301         } else {
 302             rule.setGuardExpr(guard);
 303         }
 304
 305         /* inclusion constraint */
 306         Inclusion inclusion = parse_inclusion(pn.getChild("inclusion"));
 307
 308         if (inclusion == null) {
 309             ok = false;
 310         } else {
 311             rule.setInclusion(inclusion);
 312         }
 313
 314         /* pop symbol table stack */
 315         SymbolTable st = sts.pop();
 316         sts.pop(); /* pop off globals */
 317
 318         /* make sure the stack we pop is our rule s.t. */
 319         assert st == rule.getSymbolTable();
 320         assert sts.empty();
 321
 322         /* add rule to global set */
 323         vRules.addElement(rule);
 324
 325         return ok;
 326     }
 327
 328     private Inclusion parse_inclusion(ParseNode pn) {
 329         if (!precheck(pn, "inclusion")) {
 330             return null;
 331         }
 332
 333         if (pn.getChild("set") != null) {
 334             ParseNode set = pn.getChild("set");
 335             Expr expr = parse_expr(set.getChild("expr"));
 336
 337             if (expr == null) {
 338                 return null;
 339             }
 340
 341             String setname = set.getChild("name").getTerminal();
 342             assert setname != null;
 343             SetDescriptor sd = lookupSet(setname);
 344
 345             if (sd == null) {
 346                 er.report(set.getChild("name"), "Undefined set '" + setname + "'");
 347                 return null;
 348             }
 349
 350             return new SetInclusion(expr, sd);
 351         } else if (pn.getChild("relation") != null) {
 352             ParseNode relation = pn.getChild("relation");
 353             Expr leftexpr = parse_expr(relation.getChild("left").getChild("expr"));
 354             Expr rightexpr = parse_expr(relation.getChild("right").getChild("expr"));
 355
 356             if ((leftexpr == null) || (rightexpr == null)) {
 357                 return null;
 358             }
 359
 360             String relname = relation.getChild("name").getTerminal();
 361             assert relname != null;
 362             RelationDescriptor rd = lookupRelation(relname);
 363
 364             if (rd == null) {
 365                 er.report(relation.getChild("name"), "Undefined relation '" + relname + "'");
 366                 return null;
 367             }
 368
 369             return new RelationInclusion(leftexpr, rightexpr, rd);
 370         } else {
 371             throw new IRException();
 372         }
 373     }
 374
 375     private boolean parse_constraints(ParseNode pn) {
 376         if (!precheck(pn, "constraints")) {
 377             return false;
 378         }
 379
 380         boolean ok = true;
 381         ParseNodeVector constraints = pn.getChildren();
 382
 383         for (int i = 0; i < constraints.size(); i++) {
 384             ParseNode constraint = constraints.elementAt(i);
 385             assert constraint.getLabel().equals("constraint");
 386             if (!parse_constraint(constraint)) {
 387                 ok = false;
 388             }
 389         }
 390
 391         /* do any post checks... (type constraints, etc?) */
 392
 393         return ok;
 394     }
 395
 396     private boolean parse_constraint(ParseNode pn) {
 397         if (!precheck(pn, "constraint")) {
 398             return false;
 399         }
 400
 401         boolean ok = true;
 402         Constraint constraint = new Constraint();
 403
 404         /* test crash */
 405         boolean crash = pn.getChild("crash") != null;
 406         constraint.setCrash(crash);
 407
 408         /* set up symbol table for constraint */
 409         assert sts.empty();
 410         sts.push(constraint.getSymbolTable());
 411
 412         /* get quantifiers */
 413         if (pn.getChild("quantifiers") != null) {
 414             ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
 415
 416             for (int i = 0; i < quantifiers.size(); i++) {
 417                 ParseNode qn = quantifiers.elementAt(i);
 418                 assert qn.getLabel().equals("quantifier");
 419                 Quantifier quantifier = parse_quantifier(qn);
 420                 if (quantifier == null) {
 421                     ok = false;
 422                 } else {
 423                     constraint.addQuantifier(quantifier);
 424                 }
 425             }
 426         }
 427
 428         /* get body */
 429         LogicStatement logicexpr = parse_body(pn.getChild("body"));
 430
 431         if (logicexpr == null) {
 432             ok = false;
 433         } else {
 434             constraint.setLogicStatement(logicexpr);
 435         }
 436
 437         /* pop symbol table stack */
 438         SymbolTable st = sts.pop();
 439
 440         /* make sure the stack we pop is our constraint s.t. */
 441         assert st == constraint.getSymbolTable();
 442         assert sts.empty();
 443
 444         /* add to vConstraints */
 445         vConstraints.addElement(constraint);
 446
 447         return ok;
 448     }
 449
 450     private Quantifier parse_quantifier(ParseNode pn) {
 451         if (!precheck(pn, "quantifier")) {
 452             return null;
 453         }
 454
 455         if (pn.getChild("forall") != null) { /* forall element in Set */
 456             SetQuantifier sq = new SetQuantifier();
 457
 458             /* get var */
 459             VarDescriptor vd = reserveName(pn.getChild("var"));
 460
 461             if (vd == null) {
 462                 return null;
 463             }
 464
 465             sq.setVar(vd);
 466
 467             /* parse the set */
 468             SetDescriptor set = parse_set(pn.getChild("set"));
 469             assert set != null;
 470             sq.setSet(set);
 471
 472             vd.setType(set.getType());
 473
 474             /* return to caller */
 475             return sq;
 476
 477         } else if (pn.getChild("relatiion") != null) { /* for < v1, v2 > in Relation */
 478             RelationQuantifier rq = new RelationQuantifier();
 479
 480             /* get vars */
 481             VarDescriptor vd1 = reserveName(pn.getChild("left"));
 482             VarDescriptor vd2 = reserveName(pn.getChild("right"));
 483
 484             if ((vd1 == null) || (vd2 == null)) {
 485                 return null;
 486             }
 487
 488             rq.setTuple(vd1, vd2);
 489
 490             /* get relation */
 491             String relationname = pn.getChild("relation").getTerminal();
 492             assert relationname != null;
 493             RelationDescriptor rd = lookupRelation(relationname);
 494
 495             if (rd == null) {
 496                 return null;
 497             }
 498
 499             rq.setRelation(rd);
 500             vd1.setType(rd.getDomain().getType());
 501             vd2.setType(rd.getRange().getType());
 502             return rq;
 503         } else if (pn.getChild("for") != null) { /* for j = x to y */
 504             ForQuantifier fq = new ForQuantifier();
 505
 506             /* grab var */
 507             VarDescriptor vd = reserveName(pn.getChild("var"));
 508
 509             if (vd == null) {
 510                 return null;
 511             }
 512
 513             vd.setType(ReservedTypeDescriptor.INT);
 514             fq.setVar(vd);
 515
 516             /* grab lower/upper bounds */
 517             Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
 518             Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
 519
 520             if ((lower == null) || (upper == null)) {
 521                 return null;
 522             }
 523
 524             fq.setBounds(lower, upper);
 525
 526             return fq;
 527         } else {
 528             throw new IRException("not supported yet");
 529         }
 530
 531     }
 532
 533     private LogicStatement parse_body(ParseNode pn) {
 534         if (!precheck(pn, "body")) {
 535             return null;
 536         }
 537
 538         if (pn.getChild("and") != null) {
 539             /* body AND body */
 540             LogicStatement left, right;
 541             left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
 542             right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
 543
 544             if ((left == null) || (right == null)) {
 545                 return null;
 546             }
 547
 548             // what do we want to call the and/or/not body classes?
 549             return new LogicStatement(LogicStatement.AND, left, right);
 550         } else if (pn.getChild("or") != null) {
 551             /* body OR body */
 552             LogicStatement left, right;
 553             left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
 554             right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
 555
 556             if ((left == null) || (right == null)) {
 557                 return null;
 558             }
 559
 560             return new LogicStatement(LogicStatement.OR, left, right);
 561         } else if (pn.getChild("not") != null) {
 562             /* NOT body */
 563             LogicStatement left = parse_body(pn.getChild("not").getChild("left").getChild("body"));
 564
 565             if (left == null) {
 566                 return null;
 567             }
 568
 569             return new LogicStatement(LogicStatement.NOT, left);
 570         } else if (pn.getChild("predicate") != null) {
 571             return parse_predicate(pn.getChild("predicate"));
 572         } else {
 573             throw new IRException();
 574         }
 575     }
 576
 577     private Predicate parse_predicate(ParseNode pn) {
 578         if (!precheck(pn, "predicate")) {
 579             return null;
 580         }
 581
 582         if (pn.getChild("inclusion") != null) {
 583             ParseNode in = pn.getChild("inclusion");
 584
 585             /* get quantiifer var */
 586             VarDescriptor vd = parse_quantifiervar(in.getChild("quantifiervar"));
 587
 588             if (vd == null) {
 589                 return null;
 590             }
 591
 592             /* get set expr */
 593             SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
 594
 595             if (setexpr == null) {
 596                 return null;
 597             }
 598
 599             return new InclusionPredicate(vd, setexpr);
 600         } else if (pn.getChild("sizeof") != null) {
 601             ParseNode sizeof = pn.getChild("sizeof");
 602
 603             /* get set expr */
 604             SetExpr setexpr = parse_setexpr(sizeof.getChild("setexpr"));
 605
 606             if (setexpr == null) {
 607                 return null;
 608             }
 609
 610             /* get comparison operator */
 611             String compareop = sizeof.getChild("compare").getTerminal();
 612             Opcode opcode = Opcode.decodeFromString(compareop);
 613
 614             if (opcode == null) {
 615                 er.report(pn, "Unsupported operation '" + compareop + "'");
 616                 return null;
 617             } else if (opcode != Opcode.EQ &&
 618                        opcode != Opcode.GE &&
 619                        opcode != Opcode.LE) {
 620                 er.report(pn, "Invalid operation '" + compareop + "': Must be one of '=', '>=', '<='");
 621                 return null;
 622             }
 623
 624             /* get decimal */
 625             String decimal = sizeof.getChild("decimal").getTerminal();
 626             IntegerLiteralExpr cardinality = new IntegerLiteralExpr(Integer.parseInt(decimal));
 627
 628             return new SizeofPredicate(setexpr, opcode, cardinality);
 629         } else if (pn.getChild("comparison") != null) {
 630             ParseNode cn = pn.getChild("comparison");
 631
 632             /* get quantifier variable */
 633             String varname = cn.getChild("quantifier").getTerminal();
 634             String relation = cn.getChild("relation").getTerminal();
 635
 636             if (!sts.peek().contains(varname)) {
 637                 er.report(pn, "Undefined quantifier '" + varname + "'");
 638                 return null;
 639             }
 640
 641             VarDescriptor vd = (VarDescriptor) sts.peek().get(varname);
 642
 643             if (!stRelations.contains(relation)) {
 644                 er.report(pn, "Undefined relation '" + varname + "'");
 645                 return null;
 646             }
 647
 648             RelationDescriptor rd = (RelationDescriptor) stRelations.get(relation);
 649
 650             /* get the expr's */
 651             Expr expr = parse_expr(cn.getChild("expr"));
 652
 653             if (expr == null) {
 654                 return null;
 655             }
 656
 657             /* get comparison operator */
 658             String compareop = cn.getChild("compare").getTerminal();
 659             Opcode opcode = Opcode.decodeFromString(compareop);
 660
 661             if (opcode == null) {
 662                 er.report(pn, "Unsupported operation '" + compareop + "'");
 663                 return null;
 664             } else if (opcode != Opcode.EQ &&
 665                        opcode != Opcode.GE &&
 666                        opcode != Opcode.LE) {
 667                 er.report(pn, "Invalid operation '" + compareop + "': Must be one of '=', '>=', '<='");
 668                 return null;
 669             }
 670
 671             return new ComparisonPredicate(vd, rd, opcode, expr);
 672         } else {
 673             throw new IRException();
 674         }
 675     }
 676
 677     private SetDescriptor parse_set(ParseNode pn) {
 678         if (!precheck(pn, "set")) {
 679             return null;
 680         }
 681
 682         if (pn.getChild("name") != null) {
 683             String setname = pn.getChild("name").getTerminal();
 684             assert setname != null;
 685
 686             if (!stSets.contains(setname)) {
 687                 /* Semantic Error: unknown set */
 688                 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
 689                 return null;
 690             } else {
 691                 /* all good, get setdescriptor */
 692                 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
 693                 assert sd != null;
 694                 return sd;
 695             }
 696         } else if (pn.getChild("listofliterals") != null) {
 697             TokenSetDescriptor tokenset = new TokenSetDescriptor();
 698             ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
 699             assert token_literals.size() > 0;
 700
 701             for (int i = 0; i < token_literals.size(); i++) {
 702                 ParseNode literal = token_literals.elementAt(i);
 703                 assert literal.getLabel().equals("literal");
 704                 LiteralExpr litexpr = parse_literal(literal);
 705
 706                 if (litexpr == null) {
 707                     return null;
 708                 }
 709
 710                 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
 711                     tokenset.addLiteral(litexpr);
 712                 } else {
 713                     er.report(literal, "Elements of a user-defined set must be of type token or integer");
 714                     // return null; /* don't think we need to return null */
 715                 }
 716             }
 717
 718             return tokenset;
 719         } else {
 720             throw new IRException(pn.getTerminal());
 721         }
 722     }
 723
 724     private boolean parse_space(ParseNode pn) {
 725         if (!precheck(pn, "space")) {
 726             return false;
 727         }
 728
 729         boolean ok = true;
 730         ParseNodeVector sets = pn.getChildren("setdefinition");
 731         ParseNodeVector relations = pn.getChildren("relationdefinition");
 732
 733         assert pn.getChildren().size() == (sets.size() + relations.size());
 734
 735         /* parse sets */
 736         for (int i = 0; i < sets.size(); i++) {
 737             if (!parse_setdefinition(sets.elementAt(i))) {
 738                 ok = false;
 739             }
 740         }
 741
 742         /* parse relations */
 743         for (int i = 0; i < relations.size(); i++) {
 744             if (!parse_relationdefinition(relations.elementAt(i))) {
 745                 ok = false;
 746             }
 747         }
 748
 749         // ok, all the spaces have been parsed, now we should typecheck and check
 750         // for cycles etc.
 751
 752         // #TBD#: typecheck and check for cycles
 753
 754         /* replace missing with actual */
 755         Iterator allsets = state.stSets.descriptors();
 756
 757         while (allsets.hasNext()) {
 758             SetDescriptor sd = (SetDescriptor) allsets.next();
 759             Vector subsets = sd.getSubsets();
 760
 761             for (int i = 0; i < subsets.size(); i++) {
 762                 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
 763
 764                 if (subset instanceof MissingSetDescriptor) {
 765                     SetDescriptor newsubset = lookupSet(subset.getSymbol());
 766
 767                     if (newsubset == null) {
 768                         er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
 769                     } else {
 770                         subsets.setElementAt(newsubset, i);
 771                     }
 772                 }
 773             }
 774         }
 775
 776         return ok;
 777     }
 778
 779     private boolean parse_setdefinition(ParseNode pn) {
 780         if (!precheck(pn, "setdefinition")) {
 781             return false;
 782         }
 783
 784         boolean ok = true;
 785
 786         /* get set name */
 787         String setname = pn.getChild("name").getTerminal();
 788         assert (setname != null);
 789
 790         SetDescriptor sd = new SetDescriptor(setname);
 791
 792         /* get set type */
 793         String settype = pn.getChild("type").getTerminal();
 794         TypeDescriptor type = lookupType(settype);
 795         if (type == null) {
 796             er.report(pn, "Undefined type '" + settype + "'");
 797             ok = false;
 798         } else {
 799             sd.setType(type);
 800         }
 801
 802         /* is this a partition? */
 803         boolean partition = pn.getChild("partition") != null;
 804         sd.isPartition(partition);
 805
 806         /* if set has subsets, add them to set descriptor */
 807         if (pn.getChild("setlist") != null) {
 808             ParseNodeVector setlist = pn.getChild("setlist").getChildren();
 809
 810             for (int i = 0; i < setlist.size(); i++) {
 811                 String subsetname = setlist.elementAt(i).getLabel();
 812                 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
 813             }
 814         }
 815
 816         /* add set to symbol table */
 817         if (stSets.contains(setname)) {
 818             // Semantic Check: redefinition
 819             er.report(pn, "Redefinition of set: " + setname);
 820             ok = false;
 821         } else {
 822             stSets.add(sd);
 823         }
 824
 825         return ok;
 826     }
 827
 828     private boolean parse_relationdefinition(ParseNode pn) {
 829         if (!precheck(pn, "relationdefinition")) {
 830             return false;
 831         }
 832
 833         boolean ok = true;
 834
 835         /* get relation name */
 836         String relname = pn.getChild("name").getTerminal();
 837         assert relname != null;
 838
 839         RelationDescriptor rd = new RelationDescriptor(relname);
 840
 841         /* check if static */
 842         boolean bStatic = pn.getChild("static") != null;
 843         rd.isStatic(bStatic);
 844
 845         /* get domain */
 846         String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
 847         assert domainsetname != null;
 848
 849         /* get range */
 850         String rangesetname = pn.getChild("range").getChild("type").getTerminal();
 851         assert rangesetname != null;
 852
 853         /* get domain multiplicity */
 854         String domainmult = pn.getChild("domain").getChild("mult").getTerminal();
 855         assert domainmult != null;
 856
 857         /* get range multiplicity */
 858         String rangemult = pn.getChild("range").getChild("mult").getTerminal();
 859         assert rangemult != null;
 860
 861         /* NOTE: it is assumed that the sets have been parsed already so that the
 862            set namespace is fully populated. any missing setdescriptors for the set
 863            symbol table will be assumed to be errors and reported. */
 864
 865         SetDescriptor domainset = lookupSet(domainsetname);
 866         if (domainset == null) {
 867             er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
 868             ok = false;
 869         } else {
 870             rd.setDomain(domainset);
 871         }
 872
 873         SetDescriptor rangeset = lookupSet(rangesetname);
 874         if (rangeset == null) {
 875             er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
 876             ok = false;
 877         } else {
 878             rd.setRange(rangeset);
 879         }
 880
 881         // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
 882
 883         /* lets add the relation to the global symbol table */
 884         if (!stRelations.contains(relname)) {
 885             stRelations.add(rd);
 886         } else {
 887             er.report(pn, "Redefinition of relation '" + relname + "'");
 888             ok = false;
 889         }
 890
 891         return ok;
 892     }
 893
 894     private boolean parse_structures(ParseNode pn) {
 895         if (!precheck(pn, "structures")) {
 896             return false;
 897         }
 898
 899         boolean ok = true;
 900         ParseNodeVector structures = pn.getChildren("structure");
 901
 902         for (int i = 0; i < structures.size(); i++) {
 903             if (!parse_structure(structures.elementAt(i))) {
 904                 ok = false;
 905             }
 906         }
 907
 908         ParseNodeVector globals = pn.getChildren("global");
 909
 910         for (int i = 0; i < globals.size(); i++) {
 911             if (!parse_global(globals.elementAt(i))) {
 912                 ok = false;
 913             }
 914         }
 915
 916         // ok, all the structures have been parsed, now we gotta type check
 917
 918         Enumeration types = stTypes.getDescriptors();
 919         while (types.hasMoreElements()) {
 920             TypeDescriptor t = (TypeDescriptor) types.nextElement();
 921
 922             if (t instanceof ReservedTypeDescriptor) {
 923                 // we don't need to check reserved types
 924             } else if (t instanceof StructureTypeDescriptor) {
 925
 926                 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
 927                 TypeDescriptor subtype = type.getSubType();
 928
 929                 // check that the subtype is valid
 930                 if (subtype instanceof MissingTypeDescriptor) {
 931                     TypeDescriptor newtype = lookupType(subtype.getSymbol());
 932                     if (newtype == null) {
 933                         // subtype not defined anywheere
 934                         // #TBD#: somehow determine how we can get the original parsenode (global function?)
 935                         er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
 936                         ok = false;
 937                     } else {
 938                         type.setSubType(newtype);
 939                     }
 940                 }
 941
 942                 Iterator fields = type.getFields();
 943
 944                 while (fields.hasNext()) {
 945                     FieldDescriptor field = (FieldDescriptor) fields.next();
 946                     TypeDescriptor fieldtype = field.getType();
 947
 948                     assert fieldtype != null;
 949
 950                     // check that the type is valid
 951                     if (fieldtype instanceof MissingTypeDescriptor) {
 952                         TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
 953                         if (newtype == null) {
 954                             // type never defined
 955                             // #TBD#: replace new ParseNode with original parsenode
 956                             er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
 957                             ok = false;
 958                         } else {
 959                             assert newtype != null;
 960                             field.setType(newtype);
 961                         }
 962                     }
 963                 }
 964
 965                 Iterator labels = type.getLabels();
 966
 967                 while (labels.hasNext()) {
 968                     LabelDescriptor label = (LabelDescriptor) labels.next();
 969                     TypeDescriptor labeltype = label.getType();
 970
 971                     assert labeltype != null;
 972
 973                     // check that the type is valid
 974                     if (labeltype instanceof MissingTypeDescriptor) {
 975                         TypeDescriptor newtype = lookupType(labeltype.getSymbol());
 976                         if (newtype == null) {
 977                             // type never defined
 978                             // #TBD#: replace new ParseNode with original parsenode
 979                             er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
 980                             ok = false;
 981                         } else {
 982                             assert newtype != null;
 983                             label.setType(newtype);
 984                         }
 985                     }
 986                 }
 987
 988             } else {
 989                 throw new IRException("shouldn't be any other typedescriptor classes");
 990             }
 991         }
 992
 993         if (!ok) {
 994             return false;
 995         }
 996
 997         types = stTypes.getDescriptors();
 998
 999         while (types.hasMoreElements()) {
1000             TypeDescriptor t = (TypeDescriptor) types.nextElement();
1001
1002             if (t instanceof ReservedTypeDescriptor) {
1003                 // we don't need to check reserved types
1004             } else if (t instanceof StructureTypeDescriptor) {
1005
1006                 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
1007                 TypeDescriptor subtype = type.getSubType();
1008                 Iterator fields = type.getFields();
1009
1010                 while (fields.hasNext()) {
1011                     FieldDescriptor field = (FieldDescriptor) fields.next();
1012
1013                     if (field instanceof ArrayDescriptor) {
1014                         ArrayDescriptor ad = (ArrayDescriptor) field;
1015                         Expr indexbound = ad.getIndexBound();
1016                         TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
1017                                 public IRErrorReporter getErrorReporter() { return er; }
1018                                 public SymbolTable getSymbolTable() { return stGlobals; }
1019                             });
1020
1021                         if (indextype == null) {
1022                             ok = false;
1023                         } else if (indextype != ReservedTypeDescriptor.INT) {
1024                             er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
1025                             ok = false;
1026                         }
1027                     }
1028                 }
1029
1030                 Iterator labels = type.getLabels();
1031
1032                 while (labels.hasNext()) {
1033                     LabelDescriptor label = (LabelDescriptor) labels.next();
1034                     Expr index = label.getIndex();
1035
1036                     if (index != null) {
1037                         TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
1038                                 public IRErrorReporter getErrorReporter() { return er; }
1039                                 public SymbolTable getSymbolTable() { return stGlobals; }
1040                             });
1041
1042                         if (indextype != ReservedTypeDescriptor.INT) {
1043                             er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
1044                             ok = false;
1045                         }
1046                     }
1047                 }
1048
1049             } else {
1050                 throw new IRException("shouldn't be any other typedescriptor classes");
1051             }
1052
1053         }
1054
1055         // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
1056         // subtypes, of course, are not real subtypes, they are merely a way to validate a
1057         // cast, i believe
1058
1059         return ok;
1060     }
1061
1062     private boolean parse_global(ParseNode pn) {
1063         if (!precheck(pn, "global")) {
1064             return false;
1065         }
1066
1067         String name = pn.getChild("name").getTerminal();
1068         assert name != null;
1069
1070         String type = pn.getChild("type").getTerminal();
1071         assert type != null;
1072         TypeDescriptor td = lookupType(type);
1073         assert td != null;
1074         assert !(td instanceof ReservedTypeDescriptor);
1075
1076         if (stGlobals.contains(name)) {
1077             /* redefinition of global */
1078             er.report(pn, "Redefinition of global '" + name + "'");
1079             return false;
1080         }
1081
1082         stGlobals.add(new VarDescriptor(name, name, td));
1083         return true;
1084     }
1085
1086     private boolean parse_structure(ParseNode pn) {
1087         if (!precheck(pn, "structure")) {
1088             return false;
1089         }
1090
1091         boolean ok = true;
1092         String typename = pn.getChild("name").getTerminal();
1093         StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1094
1095         if (pn.getChild("subtype") != null) {
1096             // has a subtype, lets try to resolve it
1097             String subtype = pn.getChild("subtype").getTerminal();
1098
1099             if (subtype.equals(typename)) {
1100                 // Semantic Error: cyclic inheritance
1101                 er.report(pn, "Cyclic inheritance prohibited");
1102                 ok = false;
1103             }
1104
1105             /* lookup the type to get the type descriptor */
1106             type.setSubType(lookupType(subtype, CREATE_MISSING));
1107         }
1108
1109         // set the current type so that the recursive parses on the labels
1110         // and fields can add themselves automatically to the current type
1111         dCurrentType = type;
1112
1113         // parse the labels and fields
1114         if (!parse_labelsandfields(pn.getChild("lf"))) {
1115             ok = false;
1116         }
1117
1118         if (stTypes.contains(typename)) {
1119             er.report(pn, "Redefinition of type '" + typename + "'");
1120             ok = false;
1121         } else {
1122             stTypes.add(type);
1123         }
1124
1125         return ok;
1126     }
1127
1128     private boolean parse_labelsandfields(ParseNode pn) {
1129         if (!precheck(pn, "lf")) {
1130             return false;
1131         }
1132
1133         boolean ok = true;
1134
1135         // check the fields first (need the field names
1136         // to type check the labels)
1137         if (!parse_fields(pn.getChild("fields"))) {
1138             ok = false;
1139         }
1140
1141         // check the labels now that all the fields are sorted
1142         if (!parse_labels(pn.getChild("labels"))) {
1143             ok = false;
1144         }
1145
1146         return ok;
1147     }
1148
1149     private boolean parse_fields(ParseNode pn) {
1150         if (!precheck(pn, "fields")) {
1151             return false;
1152         }
1153
1154         boolean ok = true;
1155
1156         /* NOTE: because the order of the fields is important when defining a data structure,
1157            and because the order is defined by the order of the fields defined in the field
1158            vector, its important that the parser returns the fields in the correct order */
1159
1160         ParseNodeVector fields = pn.getChildren();
1161
1162         for (int i = 0; i < fields.size(); i++) {
1163             ParseNode field = fields.elementAt(i);
1164             FieldDescriptor fd;
1165             boolean reserved;
1166             String name = null;
1167
1168             if (field.getChild("reserved") != null) {
1169                 // reserved field
1170                 // #TBD#: it will be necessary for reserved field descriptors to generate
1171                 // a unique symbol for the type descriptor requires it for its hashtable
1172                 fd = new ReservedFieldDescriptor();
1173                 reserved = true;
1174             } else {
1175                 name = field.getChild("name").getTerminal();
1176                 fd = new FieldDescriptor(name);
1177                 reserved = false;
1178             }
1179
1180             String type = field.getChild("type").getTerminal();
1181             boolean ptr = field.getChild("*") != null;
1182             fd.setPtr(ptr);
1183
1184             fd.setType(lookupType(type, CREATE_MISSING));
1185
1186             if (field.getChild("index") != null) {
1187                 // field is an array, so create an array descriptor to wrap the
1188                 // field descriptor and then replace the top level field descriptor with
1189                 // this array descriptor
1190                 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1191                 if (expr == null) {
1192                     // #ATTN#: do we really want to return an exception here?
1193                     throw new IRException("invalid index expression");
1194                 }
1195                 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1196                 fd = ad;
1197             }
1198
1199             // add the current field to the current type
1200             if (reserved == false) {
1201                 // lets double check that we are redefining a field
1202                 if (dCurrentType.getField(name) != null) {
1203                     // Semantic Error: field redefinition
1204                     er.report(pn, "Redefinition of field '" + name + "'");
1205                     ok = false;
1206                 } else {
1207                     dCurrentType.addField(fd);
1208                 }
1209             } else {
1210                 dCurrentType.addField(fd);
1211             }
1212         }
1213
1214         return ok;
1215     }
1216
1217     private boolean parse_labels(ParseNode pn) {
1218         if (!precheck(pn, "labels")) {
1219             return false;
1220         }
1221
1222         boolean ok = true;
1223
1224         /* NOTE: parse_labels should be called after the fields have been parsed because any
1225            labels not found in the field set of the current type will be flagged as errors */
1226
1227         ParseNodeVector labels = pn.getChildren();
1228
1229         for (int i = 0; i < labels.size(); i++) {
1230             ParseNode label = labels.elementAt(i);
1231             String name = label.getChild("name").getTerminal();
1232             LabelDescriptor ld = new LabelDescriptor(name);
1233
1234             if (label.getChild("index") != null) {
1235                 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1236                 if (expr == null) {
1237                     /* #ATTN#: do we really want to return an exception here? */
1238                     throw new IRException("Invalid expression");
1239                 }
1240                 ld.setIndex(expr);
1241             }
1242
1243             String type = label.getChild("type").getTerminal();
1244
1245             ld.setType(lookupType(type, CREATE_MISSING));
1246
1247             String field = label.getChild("field").getTerminal();
1248             FieldDescriptor fd = dCurrentType.getField(field);
1249
1250             if (fd == null) {
1251                 /* Semantic Error: Undefined field in label */
1252                 er.report(label, "Undefined field '" + field + "' in label");
1253                 ok = false;
1254             } else {
1255                 ld.setField(fd);
1256             }
1257
1258             /* add label to current type */
1259             if (dCurrentType.getLabel(name) != null) {
1260                 /* semantic error: label redefinition */
1261                 er.report(pn, "Redefinition of label '" + name + "'");
1262                 ok = false;
1263             } else {
1264                 dCurrentType.addLabel(ld);
1265             }
1266         }
1267
1268         return ok;
1269     }
1270
1271     private Expr parse_expr(ParseNode pn) {
1272         if (!precheck(pn, "expr")) {
1273             return null;
1274         }
1275
1276         if (pn.getChild("var") != null) {
1277             // we've got a variable reference... we'll have to scope check it later
1278             // when we are completely done... there are also some issues of cyclic definitions
1279             return new VarExpr(pn.getChild("var").getTerminal());
1280         } else if (pn.getChild("literal") != null) {
1281             return parse_literal(pn.getChild("literal"));
1282         } else if (pn.getChild("operator") != null) {
1283             return parse_operator(pn.getChild("operator"));
1284         } else if (pn.getChild("relation") != null) {
1285             return parse_relation(pn.getChild("relation"));
1286         } else if (pn.getChild("sizeof") != null) {
1287             return parse_sizeof(pn.getChild("sizeof"));
1288         } else if (pn.getChild("simple_expr") != null) {
1289             return parse_simple_expr(pn.getChild("simple_expr"));
1290         } else if (pn.getChild("elementof") != null) {
1291             return parse_elementof(pn.getChild("elementof"));
1292         } else if (pn.getChild("tupleof") != null) {
1293             return parse_tupleof(pn.getChild("tupleof"));
1294         } else if (pn.getChild("isvalid") != null) {
1295             er.report(pn, "Operation 'isvalid' is currently unsupported.");
1296             return null;
1297         } else {
1298             er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1299             return null;
1300         }
1301     }
1302
1303     private Expr parse_elementof(ParseNode pn) {
1304         if (!precheck(pn, "elementof")) {
1305             return null;
1306         }
1307
1308         /* get setname */
1309         String setname = pn.getChild("name").getTerminal();
1310         assert setname != null;
1311         SetDescriptor sd = lookupSet(setname);
1312
1313         if (sd == null) {
1314             er.report(pn, "Undefined set '" + setname + "'");
1315             return null;
1316         }
1317
1318         /* get left side expr */
1319         Expr expr = parse_expr(pn.getChild("expr"));
1320
1321         if (expr == null) {
1322             return null;
1323         }
1324
1325         return new ElementOfExpr(expr, sd);
1326     }
1327
1328     private Expr parse_tupleof(ParseNode pn) {
1329         if (!precheck(pn, "tupleof")) {
1330             return null;
1331         }
1332
1333         /* get relation */
1334         String relname = pn.getChild("name").getTerminal();
1335         assert relname != null;
1336         RelationDescriptor rd = lookupRelation(relname);
1337
1338         if (rd == null) {
1339             er.report(pn, "Undefined relation '" + relname + "'");
1340             return null;
1341         }
1342
1343         Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1344         Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1345
1346         if ((left == null) || (right == null)) {
1347             return null;
1348         }
1349
1350         return new TupleOfExpr(left, right, rd);
1351     }
1352
1353     private Expr parse_simple_expr(ParseNode pn) {
1354         if (!precheck(pn, "simple_expr")) {
1355             return null;
1356         }
1357
1358         // only locations so far
1359         return parse_location(pn.getChild("location"));
1360     }
1361
1362     private Expr parse_location(ParseNode pn) {
1363         if (!precheck(pn, "location")) {
1364             return null;
1365         }
1366
1367         if (pn.getChild("var") != null) {
1368             // should be changed into a namespace check */
1369             return new VarExpr(pn.getChild("var").getTerminal());
1370         } else if (pn.getChild("cast") != null) {
1371             return parse_cast(pn.getChild("cast"));
1372         } else if (pn.getChild("dot") != null) {
1373             return parse_dot(pn.getChild("dot"));
1374         } else {
1375             throw new IRException();
1376         }
1377     }
1378
1379     private RelationExpr parse_relation(ParseNode pn) {
1380         if (!precheck(pn, "relation")) {
1381             return null;
1382         }
1383
1384         String relname = pn.getChild("name").getTerminal();
1385         boolean inverse = pn.getChild("inv") == null;
1386         Expr expr = parse_expr(pn.getChild("expr"));
1387
1388         if (expr == null) {
1389             return null;
1390         }
1391
1392         RelationDescriptor relation = lookupRelation(relname);
1393
1394         if (relation == null) {
1395             /* Semantic Error: relation not definied" */
1396             er.report(pn, "Undefined relation '" + relname + "'");
1397             return null;
1398         }
1399
1400         return new RelationExpr(expr, relation, inverse);
1401     }
1402
1403     private SizeofExpr parse_sizeof(ParseNode pn) {
1404         if (!precheck(pn, "sizeof")) {
1405             return null;
1406         }
1407
1408         /* get setexpr */
1409         SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1410
1411         if (setexpr == null) {
1412             return null;
1413         }
1414
1415         return new SizeofExpr(setexpr);
1416     }
1417
1418     private CastExpr parse_cast(ParseNode pn) {
1419         if (!precheck(pn, "cast")) {
1420             return null;
1421         }
1422
1423         /* get type */
1424         String typename = pn.getChild("type").getTerminal();
1425         assert typename != null;
1426         TypeDescriptor type = lookupType(typename);
1427
1428         if (type == null) {
1429             /* semantic error: undefined type in cast */
1430             er.report(pn, "Undefined type '" + typename + "' in cast operator");
1431             return null;
1432         }
1433
1434         /* get expr */
1435         Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1436
1437         if (expr == null) {
1438             return null;
1439         }
1440
1441         return new CastExpr(type, expr);
1442     }
1443
1444     private SetExpr parse_setexpr(ParseNode pn) {
1445         if (!precheck(pn, "setexpr")) {
1446             return null;
1447         }
1448
1449         // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1450
1451         if (pn.getChild("set") != null) {
1452             String setname = pn.getChild("set").getTerminal();
1453             assert setname != null;
1454             SetDescriptor sd = lookupSet(setname);
1455
1456             if (sd == null) {
1457                 er.report(pn, "Unknown or undefined set '" + setname + "'");
1458                 return null;
1459             } else {
1460                 return new SetExpr(sd);
1461             }
1462         } else if (pn.getChild("dot") != null) {
1463             VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1464             RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1465             return new ImageSetExpr(vd, relation);
1466         } else if (pn.getChild("dotinv") != null) {
1467             VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1468             RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1469             return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1470         } else {
1471             throw new IRException();
1472         }
1473     }
1474
1475     private VarDescriptor parse_quantifiervar(ParseNode pn) {
1476         if (!precheck(pn, "quantifiervar")) {
1477             return null;
1478         }
1479
1480         /* get var */
1481         String varname = pn.getTerminal();
1482         assert varname != null;
1483
1484         /* NOTE: quantifier var's are only found in the constraints and
1485            model definitions... therefore we can do a semantic check here
1486            to make sure that the variables exist in the symbol table */
1487
1488         /* NOTE: its assumed that the symbol table stack is appropriately
1489            set up with the parent quantifier symbol table */
1490         assert !sts.empty();
1491
1492         /* do semantic check and if valid, add it to symbol table
1493            and add it to the quantifier as well */
1494         if (sts.peek().contains(varname)) {
1495             return new VarDescriptor(varname);
1496         } else {
1497             /* Semantic Error: undefined variable */
1498             er.report(pn, "Undefined variable '" + varname + "'");
1499             return null;
1500         }
1501     }
1502
1503     private LiteralExpr parse_literal(ParseNode pn) {
1504         if (!precheck(pn, "literal")) {
1505             return null;
1506         }
1507
1508         if (pn.getChild("boolean") != null) {
1509             if (pn.getChild("boolean").getChild("true") != null) {
1510                 return new BooleanLiteralExpr(true);
1511             } else {
1512                 return new BooleanLiteralExpr(false);
1513             }
1514         } else if (pn.getChild("decimal") != null) {
1515             String integer = pn.getChild("decimal").getTerminal();
1516
1517             /* Check for integer literal overflow */
1518             BigInteger intLitBI = new BigInteger(integer);
1519             BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1520             BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1521             int value;
1522
1523             if (intLitBI.compareTo(intMin) < 0) {
1524                 value = Integer.MIN_VALUE;
1525                 er.warn(pn, "Integer literal overflow");
1526             } else if (intLitBI.compareTo(intMax) > 0) {
1527                 value = Integer.MAX_VALUE;
1528                 er.warn(pn, "Integer literal overflow");
1529             } else {
1530                 /* no truncation needed */
1531                 value = Integer.parseInt(integer);
1532             }
1533
1534             return new IntegerLiteralExpr(value);
1535         } else if (pn.getChild("token") != null) {
1536             return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1537         } else if (pn.getChild("string") != null) {
1538             throw new IRException("string unsupported");
1539         } else if (pn.getChild("char") != null) {
1540             throw new IRException("char unsupported");
1541         } else {
1542             throw new IRException("unknown literal expression type.");
1543         }
1544     }
1545
1546     private OpExpr parse_operator(ParseNode pn) {
1547         if (!precheck(pn, "operator")) {
1548             return null;
1549         }
1550
1551         String opname = pn.getChild("op").getTerminal();
1552         Opcode opcode = Opcode.decodeFromString(opname);
1553
1554         if (opcode == null) {
1555             er.report(pn, "Unsupported operation: " + opname);
1556             return null;
1557         }
1558
1559         Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1560         Expr right = null;
1561
1562         if (pn.getChild("right") != null) {
1563             right = parse_expr(pn.getChild("right").getChild("expr"));
1564         }
1565
1566         if (left == null) {
1567             return null;
1568         }
1569
1570         if (right == null && opcode != Opcode.NOT) {
1571             er.report(pn, "Two arguments required.");
1572             return null;
1573         }
1574
1575         return new OpExpr(opcode, left, right);
1576     }
1577
1578     private DotExpr parse_dot(ParseNode pn) {
1579         if (!precheck(pn, "dot")) {
1580             return null;
1581         }
1582
1583         Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1584
1585         if (left == null) {
1586             return null;
1587         }
1588
1589         String field = pn.getChild("field").getTerminal();
1590
1591         Expr index = null;
1592
1593         if (pn.getChild("index") != null) {
1594             index = parse_expr(pn.getChild("index").getChild("expr"));
1595
1596             if (index == null) {
1597                 return null;
1598             }
1599         }
1600
1601         return new DotExpr(left, field, index);
1602     }
1603
1604 }
1605