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             rd.addUsage(RelationDescriptor.IMAGE);
 672
 673             return new ComparisonPredicate(vd, rd, opcode, expr);
 674         } else {
 675             throw new IRException();
 676         }
 677     }
 678
 679     private SetDescriptor parse_set(ParseNode pn) {
 680         if (!precheck(pn, "set")) {
 681             return null;
 682         }
 683
 684         if (pn.getChild("name") != null) {
 685             String setname = pn.getChild("name").getTerminal();
 686             assert setname != null;
 687
 688             if (!stSets.contains(setname)) {
 689                 /* Semantic Error: unknown set */
 690                 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
 691                 return null;
 692             } else {
 693                 /* all good, get setdescriptor */
 694                 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
 695                 assert sd != null;
 696                 return sd;
 697             }
 698         } else if (pn.getChild("listofliterals") != null) {
 699             TokenSetDescriptor tokenset = new TokenSetDescriptor();
 700             ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
 701             assert token_literals.size() > 0;
 702
 703             for (int i = 0; i < token_literals.size(); i++) {
 704                 ParseNode literal = token_literals.elementAt(i);
 705                 assert literal.getLabel().equals("literal");
 706                 LiteralExpr litexpr = parse_literal(literal);
 707
 708                 if (litexpr == null) {
 709                     return null;
 710                 }
 711
 712                 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
 713                     tokenset.addLiteral(litexpr);
 714                 } else {
 715                     er.report(literal, "Elements of a user-defined set must be of type token or integer");
 716                     // return null; /* don't think we need to return null */
 717                 }
 718             }
 719
 720             return tokenset;
 721         } else {
 722             throw new IRException(pn.getTerminal());
 723         }
 724     }
 725
 726     private boolean parse_space(ParseNode pn) {
 727         if (!precheck(pn, "space")) {
 728             return false;
 729         }
 730
 731         boolean ok = true;
 732         ParseNodeVector sets = pn.getChildren("setdefinition");
 733         ParseNodeVector relations = pn.getChildren("relationdefinition");
 734
 735         assert pn.getChildren().size() == (sets.size() + relations.size());
 736
 737         /* parse sets */
 738         for (int i = 0; i < sets.size(); i++) {
 739             if (!parse_setdefinition(sets.elementAt(i))) {
 740                 ok = false;
 741             }
 742         }
 743
 744         /* parse relations */
 745         for (int i = 0; i < relations.size(); i++) {
 746             if (!parse_relationdefinition(relations.elementAt(i))) {
 747                 ok = false;
 748             }
 749         }
 750
 751         // ok, all the spaces have been parsed, now we should typecheck and check
 752         // for cycles etc.
 753
 754         // #TBD#: typecheck and check for cycles
 755
 756         /* replace missing with actual */
 757         Iterator allsets = state.stSets.descriptors();
 758
 759         while (allsets.hasNext()) {
 760             SetDescriptor sd = (SetDescriptor) allsets.next();
 761             Vector subsets = sd.getSubsets();
 762
 763             for (int i = 0; i < subsets.size(); i++) {
 764                 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
 765
 766                 if (subset instanceof MissingSetDescriptor) {
 767                     SetDescriptor newsubset = lookupSet(subset.getSymbol());
 768
 769                     if (newsubset == null) {
 770                         er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
 771                     } else {
 772                         subsets.setElementAt(newsubset, i);
 773                     }
 774                 }
 775             }
 776         }
 777
 778         return ok;
 779     }
 780
 781     private boolean parse_setdefinition(ParseNode pn) {
 782         if (!precheck(pn, "setdefinition")) {
 783             return false;
 784         }
 785
 786         boolean ok = true;
 787
 788         /* get set name */
 789         String setname = pn.getChild("name").getTerminal();
 790         assert (setname != null);
 791
 792         SetDescriptor sd = new SetDescriptor(setname);
 793
 794         /* get set type */
 795         String settype = pn.getChild("type").getTerminal();
 796         TypeDescriptor type = lookupType(settype);
 797         if (type == null) {
 798             er.report(pn, "Undefined type '" + settype + "'");
 799             ok = false;
 800         } else {
 801             sd.setType(type);
 802         }
 803
 804         /* is this a partition? */
 805         boolean partition = pn.getChild("partition") != null;
 806         sd.isPartition(partition);
 807
 808         /* if set has subsets, add them to set descriptor */
 809         if (pn.getChild("setlist") != null) {
 810             ParseNodeVector setlist = pn.getChild("setlist").getChildren();
 811
 812             for (int i = 0; i < setlist.size(); i++) {
 813                 String subsetname = setlist.elementAt(i).getLabel();
 814                 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
 815             }
 816         }
 817
 818         /* add set to symbol table */
 819         if (stSets.contains(setname)) {
 820             // Semantic Check: redefinition
 821             er.report(pn, "Redefinition of set: " + setname);
 822             ok = false;
 823         } else {
 824             stSets.add(sd);
 825         }
 826
 827         return ok;
 828     }
 829
 830     private boolean parse_relationdefinition(ParseNode pn) {
 831         if (!precheck(pn, "relationdefinition")) {
 832             return false;
 833         }
 834
 835         boolean ok = true;
 836
 837         /* get relation name */
 838         String relname = pn.getChild("name").getTerminal();
 839         assert relname != null;
 840
 841         RelationDescriptor rd = new RelationDescriptor(relname);
 842
 843         /* check if static */
 844         boolean bStatic = pn.getChild("static") != null;
 845         rd.isStatic(bStatic);
 846
 847         /* get domain */
 848         String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
 849         assert domainsetname != null;
 850
 851         /* get range */
 852         String rangesetname = pn.getChild("range").getChild("type").getTerminal();
 853         assert rangesetname != null;
 854
 855         /* get domain multiplicity */
 856         String domainmult = pn.getChild("domain").getChild("mult").getTerminal();
 857         assert domainmult != null;
 858
 859         /* get range multiplicity */
 860         String rangemult = pn.getChild("range").getChild("mult").getTerminal();
 861         assert rangemult != null;
 862
 863         /* NOTE: it is assumed that the sets have been parsed already so that the
 864            set namespace is fully populated. any missing setdescriptors for the set
 865            symbol table will be assumed to be errors and reported. */
 866
 867         SetDescriptor domainset = lookupSet(domainsetname);
 868         if (domainset == null) {
 869             er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
 870             ok = false;
 871         } else {
 872             rd.setDomain(domainset);
 873         }
 874
 875         SetDescriptor rangeset = lookupSet(rangesetname);
 876         if (rangeset == null) {
 877             er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
 878             ok = false;
 879         } else {
 880             rd.setRange(rangeset);
 881         }
 882
 883         // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
 884
 885         /* lets add the relation to the global symbol table */
 886         if (!stRelations.contains(relname)) {
 887             stRelations.add(rd);
 888         } else {
 889             er.report(pn, "Redefinition of relation '" + relname + "'");
 890             ok = false;
 891         }
 892
 893         return ok;
 894     }
 895
 896     private boolean parse_structures(ParseNode pn) {
 897         if (!precheck(pn, "structures")) {
 898             return false;
 899         }
 900
 901         boolean ok = true;
 902         ParseNodeVector structures = pn.getChildren("structure");
 903
 904         for (int i = 0; i < structures.size(); i++) {
 905             if (!parse_structure(structures.elementAt(i))) {
 906                 ok = false;
 907             }
 908         }
 909
 910         ParseNodeVector globals = pn.getChildren("global");
 911
 912         for (int i = 0; i < globals.size(); i++) {
 913             if (!parse_global(globals.elementAt(i))) {
 914                 ok = false;
 915             }
 916         }
 917
 918         // ok, all the structures have been parsed, now we gotta type check
 919
 920         Enumeration types = stTypes.getDescriptors();
 921         while (types.hasMoreElements()) {
 922             TypeDescriptor t = (TypeDescriptor) types.nextElement();
 923
 924             if (t instanceof ReservedTypeDescriptor) {
 925                 // we don't need to check reserved types
 926             } else if (t instanceof StructureTypeDescriptor) {
 927
 928                 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
 929                 TypeDescriptor subtype = type.getSubType();
 930
 931                 // check that the subtype is valid
 932                 if (subtype instanceof MissingTypeDescriptor) {
 933                     TypeDescriptor newtype = lookupType(subtype.getSymbol());
 934                     if (newtype == null) {
 935                         // subtype not defined anywheere
 936                         // #TBD#: somehow determine how we can get the original parsenode (global function?)
 937                         er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
 938                         ok = false;
 939                     } else {
 940                         type.setSubType(newtype);
 941                     }
 942                 }
 943
 944                 Iterator fields = type.getFields();
 945
 946                 while (fields.hasNext()) {
 947                     FieldDescriptor field = (FieldDescriptor) fields.next();
 948                     TypeDescriptor fieldtype = field.getType();
 949
 950                     assert fieldtype != null;
 951
 952                     // check that the type is valid
 953                     if (fieldtype instanceof MissingTypeDescriptor) {
 954                         TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
 955                         if (newtype == null) {
 956                             // type never defined
 957                             // #TBD#: replace new ParseNode with original parsenode
 958                             er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
 959                             ok = false;
 960                         } else {
 961                             assert newtype != null;
 962                             field.setType(newtype);
 963                         }
 964                     }
 965                 }
 966
 967                 Iterator labels = type.getLabels();
 968
 969                 while (labels.hasNext()) {
 970                     LabelDescriptor label = (LabelDescriptor) labels.next();
 971                     TypeDescriptor labeltype = label.getType();
 972
 973                     assert labeltype != null;
 974
 975                     // check that the type is valid
 976                     if (labeltype instanceof MissingTypeDescriptor) {
 977                         TypeDescriptor newtype = lookupType(labeltype.getSymbol());
 978                         if (newtype == null) {
 979                             // type never defined
 980                             // #TBD#: replace new ParseNode with original parsenode
 981                             er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
 982                             ok = false;
 983                         } else {
 984                             assert newtype != null;
 985                             label.setType(newtype);
 986                         }
 987                     }
 988                 }
 989
 990             } else {
 991                 throw new IRException("shouldn't be any other typedescriptor classes");
 992             }
 993         }
 994
 995         if (!ok) {
 996             return false;
 997         }
 998
 999         types = stTypes.getDescriptors();
1000
1001         while (types.hasMoreElements()) {
1002             TypeDescriptor t = (TypeDescriptor) types.nextElement();
1003
1004             if (t instanceof ReservedTypeDescriptor) {
1005                 // we don't need to check reserved types
1006             } else if (t instanceof StructureTypeDescriptor) {
1007
1008                 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
1009                 TypeDescriptor subtype = type.getSubType();
1010                 Iterator fields = type.getFields();
1011
1012                 while (fields.hasNext()) {
1013                     FieldDescriptor field = (FieldDescriptor) fields.next();
1014
1015                     if (field instanceof ArrayDescriptor) {
1016                         ArrayDescriptor ad = (ArrayDescriptor) field;
1017                         Expr indexbound = ad.getIndexBound();
1018                         TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
1019                                 public IRErrorReporter getErrorReporter() { return er; }
1020                                 public SymbolTable getSymbolTable() { return stGlobals; }
1021                             });
1022
1023                         if (indextype == null) {
1024                             ok = false;
1025                         } else if (indextype != ReservedTypeDescriptor.INT) {
1026                             er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
1027                             ok = false;
1028                         }
1029                     }
1030                 }
1031
1032                 Iterator labels = type.getLabels();
1033
1034                 while (labels.hasNext()) {
1035                     LabelDescriptor label = (LabelDescriptor) labels.next();
1036                     Expr index = label.getIndex();
1037
1038                     if (index != null) {
1039                         TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
1040                                 public IRErrorReporter getErrorReporter() { return er; }
1041                                 public SymbolTable getSymbolTable() { return stGlobals; }
1042                             });
1043
1044                         if (indextype != ReservedTypeDescriptor.INT) {
1045                             er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
1046                             ok = false;
1047                         }
1048                     }
1049                 }
1050
1051             } else {
1052                 throw new IRException("shouldn't be any other typedescriptor classes");
1053             }
1054
1055         }
1056
1057         // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
1058         // subtypes, of course, are not real subtypes, they are merely a way to validate a
1059         // cast, i believe
1060
1061         return ok;
1062     }
1063
1064     private boolean parse_global(ParseNode pn) {
1065         if (!precheck(pn, "global")) {
1066             return false;
1067         }
1068
1069         String name = pn.getChild("name").getTerminal();
1070         assert name != null;
1071
1072         String type = pn.getChild("type").getTerminal();
1073         assert type != null;
1074         TypeDescriptor td = lookupType(type);
1075         assert td != null;
1076         assert !(td instanceof ReservedTypeDescriptor);
1077
1078         if (stGlobals.contains(name)) {
1079             /* redefinition of global */
1080             er.report(pn, "Redefinition of global '" + name + "'");
1081             return false;
1082         }
1083
1084         stGlobals.add(new VarDescriptor(name, name, td));
1085         return true;
1086     }
1087
1088     private boolean parse_structure(ParseNode pn) {
1089         if (!precheck(pn, "structure")) {
1090             return false;
1091         }
1092
1093         boolean ok = true;
1094         String typename = pn.getChild("name").getTerminal();
1095         StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1096
1097         if (pn.getChild("subtype") != null) {
1098             // has a subtype, lets try to resolve it
1099             String subtype = pn.getChild("subtype").getTerminal();
1100
1101             if (subtype.equals(typename)) {
1102                 // Semantic Error: cyclic inheritance
1103                 er.report(pn, "Cyclic inheritance prohibited");
1104                 ok = false;
1105             }
1106
1107             /* lookup the type to get the type descriptor */
1108             type.setSubType(lookupType(subtype, CREATE_MISSING));
1109         }
1110
1111         // set the current type so that the recursive parses on the labels
1112         // and fields can add themselves automatically to the current type
1113         dCurrentType = type;
1114
1115         // parse the labels and fields
1116         if (!parse_labelsandfields(pn.getChild("lf"))) {
1117             ok = false;
1118         }
1119
1120         if (stTypes.contains(typename)) {
1121             er.report(pn, "Redefinition of type '" + typename + "'");
1122             ok = false;
1123         } else {
1124             stTypes.add(type);
1125         }
1126
1127         return ok;
1128     }
1129
1130     private boolean parse_labelsandfields(ParseNode pn) {
1131         if (!precheck(pn, "lf")) {
1132             return false;
1133         }
1134
1135         boolean ok = true;
1136
1137         // check the fields first (need the field names
1138         // to type check the labels)
1139         if (!parse_fields(pn.getChild("fields"))) {
1140             ok = false;
1141         }
1142
1143         // check the labels now that all the fields are sorted
1144         if (!parse_labels(pn.getChild("labels"))) {
1145             ok = false;
1146         }
1147
1148         return ok;
1149     }
1150
1151     private boolean parse_fields(ParseNode pn) {
1152         if (!precheck(pn, "fields")) {
1153             return false;
1154         }
1155
1156         boolean ok = true;
1157
1158         /* NOTE: because the order of the fields is important when defining a data structure,
1159            and because the order is defined by the order of the fields defined in the field
1160            vector, its important that the parser returns the fields in the correct order */
1161
1162         ParseNodeVector fields = pn.getChildren();
1163
1164         for (int i = 0; i < fields.size(); i++) {
1165             ParseNode field = fields.elementAt(i);
1166             FieldDescriptor fd;
1167             boolean reserved;
1168             String name = null;
1169
1170             if (field.getChild("reserved") != null) {
1171                 // reserved field
1172                 // #TBD#: it will be necessary for reserved field descriptors to generate
1173                 // a unique symbol for the type descriptor requires it for its hashtable
1174                 fd = new ReservedFieldDescriptor();
1175                 reserved = true;
1176             } else {
1177                 name = field.getChild("name").getTerminal();
1178                 fd = new FieldDescriptor(name);
1179                 reserved = false;
1180             }
1181
1182             String type = field.getChild("type").getTerminal();
1183             boolean ptr = field.getChild("*") != null;
1184             fd.setPtr(ptr);
1185
1186             fd.setType(lookupType(type, CREATE_MISSING));
1187
1188             if (field.getChild("index") != null) {
1189                 // field is an array, so create an array descriptor to wrap the
1190                 // field descriptor and then replace the top level field descriptor with
1191                 // this array descriptor
1192                 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1193                 if (expr == null) {
1194                     // #ATTN#: do we really want to return an exception here?
1195                     throw new IRException("invalid index expression");
1196                 }
1197                 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1198                 fd = ad;
1199             }
1200
1201             // add the current field to the current type
1202             if (reserved == false) {
1203                 // lets double check that we are redefining a field
1204                 if (dCurrentType.getField(name) != null) {
1205                     // Semantic Error: field redefinition
1206                     er.report(pn, "Redefinition of field '" + name + "'");
1207                     ok = false;
1208                 } else {
1209                     dCurrentType.addField(fd);
1210                 }
1211             } else {
1212                 dCurrentType.addField(fd);
1213             }
1214         }
1215
1216         return ok;
1217     }
1218
1219     private boolean parse_labels(ParseNode pn) {
1220         if (!precheck(pn, "labels")) {
1221             return false;
1222         }
1223
1224         boolean ok = true;
1225
1226         /* NOTE: parse_labels should be called after the fields have been parsed because any
1227            labels not found in the field set of the current type will be flagged as errors */
1228
1229         ParseNodeVector labels = pn.getChildren();
1230
1231         for (int i = 0; i < labels.size(); i++) {
1232             ParseNode label = labels.elementAt(i);
1233             String name = label.getChild("name").getTerminal();
1234             LabelDescriptor ld = new LabelDescriptor(name);
1235
1236             if (label.getChild("index") != null) {
1237                 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1238                 if (expr == null) {
1239                     /* #ATTN#: do we really want to return an exception here? */
1240                     throw new IRException("Invalid expression");
1241                 }
1242                 ld.setIndex(expr);
1243             }
1244
1245             String type = label.getChild("type").getTerminal();
1246
1247             ld.setType(lookupType(type, CREATE_MISSING));
1248
1249             String field = label.getChild("field").getTerminal();
1250             FieldDescriptor fd = dCurrentType.getField(field);
1251
1252             if (fd == null) {
1253                 /* Semantic Error: Undefined field in label */
1254                 er.report(label, "Undefined field '" + field + "' in label");
1255                 ok = false;
1256             } else {
1257                 ld.setField(fd);
1258             }
1259
1260             /* add label to current type */
1261             if (dCurrentType.getLabel(name) != null) {
1262                 /* semantic error: label redefinition */
1263                 er.report(pn, "Redefinition of label '" + name + "'");
1264                 ok = false;
1265             } else {
1266                 dCurrentType.addLabel(ld);
1267             }
1268         }
1269
1270         return ok;
1271     }
1272
1273     private Expr parse_expr(ParseNode pn) {
1274         if (!precheck(pn, "expr")) {
1275             return null;
1276         }
1277
1278         if (pn.getChild("var") != null) {
1279             // we've got a variable reference... we'll have to scope check it later
1280             // when we are completely done... there are also some issues of cyclic definitions
1281             return new VarExpr(pn.getChild("var").getTerminal());
1282         } else if (pn.getChild("literal") != null) {
1283             return parse_literal(pn.getChild("literal"));
1284         } else if (pn.getChild("operator") != null) {
1285             return parse_operator(pn.getChild("operator"));
1286         } else if (pn.getChild("relation") != null) {
1287             return parse_relation(pn.getChild("relation"));
1288         } else if (pn.getChild("sizeof") != null) {
1289             return parse_sizeof(pn.getChild("sizeof"));
1290         } else if (pn.getChild("simple_expr") != null) {
1291             return parse_simple_expr(pn.getChild("simple_expr"));
1292         } else if (pn.getChild("elementof") != null) {
1293             return parse_elementof(pn.getChild("elementof"));
1294         } else if (pn.getChild("tupleof") != null) {
1295             return parse_tupleof(pn.getChild("tupleof"));
1296         } else if (pn.getChild("isvalid") != null) {
1297             er.report(pn, "Operation 'isvalid' is currently unsupported.");
1298             return null;
1299         } else {
1300             er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1301             return null;
1302         }
1303     }
1304
1305     private Expr parse_elementof(ParseNode pn) {
1306         if (!precheck(pn, "elementof")) {
1307             return null;
1308         }
1309
1310         /* get setname */
1311         String setname = pn.getChild("name").getTerminal();
1312         assert setname != null;
1313         SetDescriptor sd = lookupSet(setname);
1314
1315         if (sd == null) {
1316             er.report(pn, "Undefined set '" + setname + "'");
1317             return null;
1318         }
1319
1320         /* get left side expr */
1321         Expr expr = parse_expr(pn.getChild("expr"));
1322
1323         if (expr == null) {
1324             return null;
1325         }
1326
1327         return new ElementOfExpr(expr, sd);
1328     }
1329
1330     private Expr parse_tupleof(ParseNode pn) {
1331         if (!precheck(pn, "tupleof")) {
1332             return null;
1333         }
1334
1335         /* get relation */
1336         String relname = pn.getChild("name").getTerminal();
1337         assert relname != null;
1338         RelationDescriptor rd = lookupRelation(relname);
1339
1340         if (rd == null) {
1341             er.report(pn, "Undefined relation '" + relname + "'");
1342             return null;
1343         }
1344
1345         Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1346         Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1347
1348         if ((left == null) || (right == null)) {
1349             return null;
1350         }
1351
1352         return new TupleOfExpr(left, right, rd);
1353     }
1354
1355     private Expr parse_simple_expr(ParseNode pn) {
1356         if (!precheck(pn, "simple_expr")) {
1357             return null;
1358         }
1359
1360         // only locations so far
1361         return parse_location(pn.getChild("location"));
1362     }
1363
1364     private Expr parse_location(ParseNode pn) {
1365         if (!precheck(pn, "location")) {
1366             return null;
1367         }
1368
1369         if (pn.getChild("var") != null) {
1370             // should be changed into a namespace check */
1371             return new VarExpr(pn.getChild("var").getTerminal());
1372         } else if (pn.getChild("cast") != null) {
1373             return parse_cast(pn.getChild("cast"));
1374         } else if (pn.getChild("dot") != null) {
1375             return parse_dot(pn.getChild("dot"));
1376         } else {
1377             throw new IRException();
1378         }
1379     }
1380
1381     private RelationExpr parse_relation(ParseNode pn) {
1382         if (!precheck(pn, "relation")) {
1383             return null;
1384         }
1385
1386         String relname = pn.getChild("name").getTerminal();
1387         boolean inverse = pn.getChild("inv") == null;
1388         Expr expr = parse_expr(pn.getChild("expr"));
1389
1390         if (expr == null) {
1391             return null;
1392         }
1393
1394         RelationDescriptor relation = lookupRelation(relname);
1395
1396         if (relation == null) {
1397             /* Semantic Error: relation not definied" */
1398             er.report(pn, "Undefined relation '" + relname + "'");
1399             return null;
1400         }
1401
1402         /* add usage so correct sets are created */
1403         relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1404
1405         return new RelationExpr(expr, relation, inverse);
1406     }
1407
1408     private SizeofExpr parse_sizeof(ParseNode pn) {
1409         if (!precheck(pn, "sizeof")) {
1410             return null;
1411         }
1412
1413         /* get setexpr */
1414         SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1415
1416         if (setexpr == null) {
1417             return null;
1418         }
1419
1420         return new SizeofExpr(setexpr);
1421     }
1422
1423     private CastExpr parse_cast(ParseNode pn) {
1424         if (!precheck(pn, "cast")) {
1425             return null;
1426         }
1427
1428         /* get type */
1429         String typename = pn.getChild("type").getTerminal();
1430         assert typename != null;
1431         TypeDescriptor type = lookupType(typename);
1432
1433         if (type == null) {
1434             /* semantic error: undefined type in cast */
1435             er.report(pn, "Undefined type '" + typename + "' in cast operator");
1436             return null;
1437         }
1438
1439         /* get expr */
1440         Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1441
1442         if (expr == null) {
1443             return null;
1444         }
1445
1446         return new CastExpr(type, expr);
1447     }
1448
1449     private SetExpr parse_setexpr(ParseNode pn) {
1450         if (!precheck(pn, "setexpr")) {
1451             return null;
1452         }
1453
1454         // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1455
1456         if (pn.getChild("set") != null) {
1457             String setname = pn.getChild("set").getTerminal();
1458             assert setname != null;
1459             SetDescriptor sd = lookupSet(setname);
1460
1461             if (sd == null) {
1462                 er.report(pn, "Unknown or undefined set '" + setname + "'");
1463                 return null;
1464             } else {
1465                 return new SetExpr(sd);
1466             }
1467         } else if (pn.getChild("dot") != null) {
1468             VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1469             RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1470             relation.addUsage(RelationDescriptor.IMAGE);
1471             return new ImageSetExpr(vd, relation);
1472         } else if (pn.getChild("dotinv") != null) {
1473             VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1474             RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1475             relation.addUsage(RelationDescriptor.INVIMAGE);
1476             return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1477         } else {
1478             throw new IRException();
1479         }
1480     }
1481
1482     private VarDescriptor parse_quantifiervar(ParseNode pn) {
1483         if (!precheck(pn, "quantifiervar")) {
1484             return null;
1485         }
1486
1487         /* get var */
1488         String varname = pn.getTerminal();
1489         assert varname != null;
1490
1491         /* NOTE: quantifier var's are only found in the constraints and
1492            model definitions... therefore we can do a semantic check here
1493            to make sure that the variables exist in the symbol table */
1494
1495         /* NOTE: its assumed that the symbol table stack is appropriately
1496            set up with the parent quantifier symbol table */
1497         assert !sts.empty();
1498
1499         /* do semantic check and if valid, add it to symbol table
1500            and add it to the quantifier as well */
1501         if (sts.peek().contains(varname)) {
1502             return new VarDescriptor(varname);
1503         } else {
1504             /* Semantic Error: undefined variable */
1505             er.report(pn, "Undefined variable '" + varname + "'");
1506             return null;
1507         }
1508     }
1509
1510     private LiteralExpr parse_literal(ParseNode pn) {
1511         if (!precheck(pn, "literal")) {
1512             return null;
1513         }
1514
1515         if (pn.getChild("boolean") != null) {
1516             if (pn.getChild("boolean").getChild("true") != null) {
1517                 return new BooleanLiteralExpr(true);
1518             } else {
1519                 return new BooleanLiteralExpr(false);
1520             }
1521         } else if (pn.getChild("decimal") != null) {
1522             String integer = pn.getChild("decimal").getTerminal();
1523
1524             /* Check for integer literal overflow */
1525             BigInteger intLitBI = new BigInteger(integer);
1526             BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1527             BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1528             int value;
1529
1530             if (intLitBI.compareTo(intMin) < 0) {
1531                 value = Integer.MIN_VALUE;
1532                 er.warn(pn, "Integer literal overflow");
1533             } else if (intLitBI.compareTo(intMax) > 0) {
1534                 value = Integer.MAX_VALUE;
1535                 er.warn(pn, "Integer literal overflow");
1536             } else {
1537                 /* no truncation needed */
1538                 value = Integer.parseInt(integer);
1539             }
1540
1541             return new IntegerLiteralExpr(value);
1542         } else if (pn.getChild("token") != null) {
1543             return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1544         } else if (pn.getChild("string") != null) {
1545             throw new IRException("string unsupported");
1546         } else if (pn.getChild("char") != null) {
1547             throw new IRException("char unsupported");
1548         } else {
1549             throw new IRException("unknown literal expression type.");
1550         }
1551     }
1552
1553     private OpExpr parse_operator(ParseNode pn) {
1554         if (!precheck(pn, "operator")) {
1555             return null;
1556         }
1557
1558         String opname = pn.getChild("op").getTerminal();
1559         Opcode opcode = Opcode.decodeFromString(opname);
1560
1561         if (opcode == null) {
1562             er.report(pn, "Unsupported operation: " + opname);
1563             return null;
1564         }
1565
1566         Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1567         Expr right = null;
1568
1569         if (pn.getChild("right") != null) {
1570             right = parse_expr(pn.getChild("right").getChild("expr"));
1571         }
1572
1573         if (left == null) {
1574             return null;
1575         }
1576
1577         if (right == null && opcode != Opcode.NOT) {
1578             er.report(pn, "Two arguments required.");
1579             return null;
1580         }
1581
1582         return new OpExpr(opcode, left, right);
1583     }
1584
1585     private DotExpr parse_dot(ParseNode pn) {
1586         if (!precheck(pn, "dot")) {
1587             return null;
1588         }
1589
1590         Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1591
1592         if (left == null) {
1593             return null;
1594         }
1595
1596         String field = pn.getChild("field").getTerminal();
1597
1598         Expr index = null;
1599
1600         if (pn.getChild("index") != null) {
1601             index = parse_expr(pn.getChild("index").getChild("expr"));
1602
1603             if (index == null) {
1604                 return null;
1605             }
1606         }
1607
1608         return new DotExpr(left, field, index);
1609     }
1610
1611 }
1612