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