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