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