Repair/RepairCompiler/MCC/IR/SemanticChecker.java

   1 package MCC.IR;
   2
   3 import java.util.*;
   4 import java.math.BigInteger;
   5 import MCC.State;
   6
   7 public class SemanticChecker {
   8
   9     private static final boolean CREATE_MISSING = true;
  10
  11     public State state;
  12
  13     Vector vConstraints;
  14     Vector vRules;
  15
  16     SymbolTableStack sts;
  17
  18     SymbolTable stSets;
  19     SymbolTable stRelations;
  20     SymbolTable stTypes;
  21     SymbolTable stGlobals;
  22
  23     StructureTypeDescriptor dCurrentType;
  24
  25     IRErrorReporter er;
  26
  27     public SemanticChecker () {
  28         dCurrentType = null;
  29         stTypes = null;
  30         er = null;
  31     }
  32
  33     public boolean check(State state, IRErrorReporter er) {
  34
  35         this.state = state;
  36         State.currentState = state;
  37
  38         if (er == null) {
  39             throw new IRException("IRBuilder.build: Received null ErrorReporter");
  40         } else {
  41             this.er = er;
  42         }
  43
  44         if (state.ptStructures == null) {
  45             throw new IRException("IRBuilder.build: Received null ParseNode");
  46         }
  47
  48         state.vConstraints = new Vector();
  49         vConstraints = state.vConstraints;
  50
  51         state.vRules = new Vector();
  52         vRules = state.vRules;
  53
  54         state.stTypes = new SymbolTable();
  55         stTypes = state.stTypes;
  56
  57         state.stSets = new SymbolTable();
  58         stSets = state.stSets;
  59
  60         state.stRelations = new SymbolTable();
  61         stRelations = state.stRelations;
  62
  63         state.stGlobals = new SymbolTable();
  64         stGlobals = state.stGlobals;
  65
  66         sts = new SymbolTableStack();
  67
  68         // add int and bool to the types list
  69         stTypes.add(ReservedTypeDescriptor.BIT);
  70         stTypes.add(ReservedTypeDescriptor.BYTE);
  71         stTypes.add(ReservedTypeDescriptor.SHORT);
  72         stTypes.add(ReservedTypeDescriptor.INT);
  73
  74         stSets.add(new ReservedSetDescriptor("int", ReservedTypeDescriptor.INT));
  75         stSets.add(new ReservedSetDescriptor("token", ReservedTypeDescriptor.INT));
  76
  77         boolean ok = true;
  78
  79         er.setFilename(state.infile + ".struct");
  80         if (!parse_structures(state.ptStructures)) {
  81
  82             ok = false;
  83             er.report(null, "Error parsing structs.");
  84         }
  85
  86         er.setFilename(state.infile + ".space");
  87         if (!parse_space(state.ptSpace)) {
  88             ok = false;
  89             er.report(null, "Error parsing sets and relations.");
  90         }
  91
  92         er.setFilename(state.infile + ".constraints");
  93         if (!parse_constraints(state.ptConstraints)) {
  94             ok = false;
  95             er.report(null, "Error parsing constraints.");
  96         }
  97
  98         er.setFilename(state.infile + ".model");
  99         if (!parse_rules(state.ptModel)) {
 100             ok = false;
 101             er.report(null, "Error parsing model definition rules.");
 102         }
 103
 104         return ok;
 105     }
 106
 107     /********************** HELPER FUNCTIONS ************************/
 108
 109     /**
 110      * special case lookup that returns null if no such type exists
 111      */
 112     private TypeDescriptor lookupType(String typename) {
 113         return lookupType(typename, false);
 114     }
 115
 116     /**
 117      * does a look up in the types symbol table. if the type is
 118      * not found than a missing type descriptor is returned
 119      */
 120     private TypeDescriptor lookupType(String typename, boolean createmissing) {
 121         if (stTypes.get(typename) != null) {
 122             // the type exists, so plug in the descriptor directly
 123             return (TypeDescriptor) stTypes.get(typename);
 124         } else if (createmissing) {
 125             return new MissingTypeDescriptor(typename);
 126         } else {
 127             return null;
 128         }
 129     }
 130
 131     /**
 132      * reserve a name
 133      */
 134     private VarDescriptor reserveName(ParseNode pn) {
 135         assert pn != null;
 136         String varname = pn.getTerminal();
 137         assert varname != null;
 138
 139         /* do semantic check and if valid, add it to symbol table
 140            and add it to the quantifier as well */
 141         if (sts.peek().contains(varname)) {
 142             /* Semantic Error: redefinition */
 143             er.report(pn, "Redefinition of '" + varname + "'");
 144             return null;
 145         } else {
 146             VarDescriptor vd = new VarDescriptor(varname);
 147             sts.peek().add(vd);
 148             return vd;
 149         }
 150     }
 151
 152     /**
 153      * special case lookup that returns null if no such set exists
 154      */
 155     private SetDescriptor lookupSet(String setname) {
 156         return lookupSet(setname, false);
 157     }
 158
 159     /**
 160      * does a look up in the set's symbol table. if the set is
 161      * not found than a missing set descriptor is returned
 162      */
 163     private SetDescriptor lookupSet(String setname, boolean createmissing) {
 164         if (stSets.get(setname) != null) {
 165             // the set exists, so plug in the descriptor directly
 166             return (SetDescriptor) stSets.get(setname);
 167         } else if (createmissing) {
 168             return new MissingSetDescriptor(setname);
 169         } else {
 170             return null;
 171         }
 172     }
 173
 174     /**
 175      * does a look up in the set's symbol table. if the set is
 176      * not found than a missing set descriptor is returned
 177      */
 178     private RelationDescriptor lookupRelation(String relname) {
 179         if (stRelations.get(relname) != null) {
 180             // the relation exists, so plug in the descriptor directly
 181             return (RelationDescriptor) stRelations.get(relname);
 182         } else {
 183             return null;
 184         }
 185     }
 186
 187
 188     private static int count = 0;
 189     private boolean precheck(ParseNode pn, String label) {
 190         if (pn == null) {
 191             er.report(pn, "IE: Expected '" + label + "', got null");
 192             assert false;
 193             return false;
 194         }
 195
 196         if (! pn.getLabel().equals(label)) {
 197             er.report(pn, "IE: Expected '" + label + "', got '" + pn.getLabel() + "'");
 198             assert false;
 199             return false;
 200         }
 201
 202         if (state.verbose >= 2) {
 203             System.err.println("visiting*" + (count++) + ": " + label);
 204         }
 205
 206         return true;
 207     }
 208
 209     /********************* PARSING FUNCTIONS ************************/
 210
 211     private boolean parse_rules(ParseNode pn) {
 212         if (!precheck(pn, "rules")) {
 213             return false;
 214         }
 215
 216         boolean ok = true;
 217         ParseNodeVector rules = pn.getChildren();
 218
 219         for (int i = 0; i < rules.size(); i++) {
 220             ParseNode rule = rules.elementAt(i);
 221             if (!parse_rule(rule)) {
 222                 er.report(rule, "Error parsing rule");
 223                 ok = false;
 224             }
 225         }
 226
 227         /* type check */
 228         Iterator ruleiterator = state.vRules.iterator();
 229
 230         while (ruleiterator.hasNext()) {
 231             Rule rule = (Rule) ruleiterator.next();
 232             Expr guard = rule.getGuardExpr();
 233             final SymbolTable rulest = rule.getSymbolTable();
 234             SemanticAnalyzer sa = new SemanticAnalyzer() {
 235                     public IRErrorReporter getErrorReporter() { return er; }
 236                     public SymbolTable getSymbolTable() { return rulest; }
 237                 };
 238             TypeDescriptor guardtype = guard.typecheck(sa);
 239
 240             if (guardtype == null) {
 241                 ok = false;
 242             } else if (guardtype != ReservedTypeDescriptor.INT) {
 243                 er.report(null, "Type of guard must be 'int' not '" + guardtype.getSymbol() + "'");
 244                 ok = false;
 245             }
 246
 247             if (!rule.getInclusion().typecheck(sa)) {
 248                 er.report(null, "Error typechecking rule:"+rule);
 249                 ok = false;
 250             }
 251
 252             Iterator quantifiers = rule.quantifiers();
 253
 254             while (quantifiers.hasNext()) {
 255                 Quantifier q = (Quantifier) quantifiers.next();
 256
 257                 if (q instanceof ForQuantifier && !((ForQuantifier)q).typecheck(sa)) {
 258                     ok = false;
 259                 }
 260             }
 261         }
 262
 263         /* do any post checks ?? */
 264
 265         return ok;
 266     }
 267
 268     private boolean parse_rule(ParseNode pn) {
 269         if (!precheck(pn, "rule")) {
 270             return false;
 271         }
 272
 273         boolean ok = true;
 274         Rule rule = new Rule();
 275
 276         /* get rule type */
 277         boolean isstatic = pn.getChild("static") != null;
 278         boolean isdelay = pn.getChild("delay") != null;
 279         rule.setStatic(isstatic);
 280         rule.setDelay(isdelay);
 281
 282         /* set up symbol table for constraint */
 283         assert sts.empty();
 284         sts.push(stGlobals);
 285         sts.push(rule.getSymbolTable());
 286         /* optional quantifiers */
 287         if (pn.getChild("quantifiers") != null) {
 288             ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
 289             for (int i = 0; i < quantifiers.size(); i++) {
 290                 ParseNode qn = quantifiers.elementAt(i);
 291                 Quantifier quantifier = parse_quantifier(qn);
 292
 293                 if (quantifier == null) {
 294                     ok = false;
 295                 } else {
 296                     rule.addQuantifier(quantifier);
 297                 }
 298             }
 299         }
 300
 301         /* get guard expr */
 302         Expr guard = parse_expr(pn.getChild("expr"));
 303
 304         if (guard == null) {
 305             ok = false;
 306         } else {
 307             rule.setGuardExpr(guard);
 308         }
 309
 310         /* inclusion constraint */
 311         Inclusion inclusion = parse_inclusion(pn.getChild("inclusion"));
 312
 313         if (inclusion == null) {
 314             ok = false;
 315         } else {
 316             rule.setInclusion(inclusion);
 317         }
 318
 319         /* pop symbol table stack */
 320         SymbolTable st = sts.pop();
 321         sts.pop(); /* pop off globals */
 322
 323         /* make sure the stack we pop is our rule s.t. */
 324         assert st == rule.getSymbolTable();
 325         assert sts.empty();
 326
 327         /* add rule to global set */
 328         vRules.addElement(rule);
 329
 330         return ok;
 331     }
 332
 333     private Inclusion parse_inclusion(ParseNode pn) {
 334         if (!precheck(pn, "inclusion")) {
 335             return null;
 336         }
 337
 338         if (pn.getChild("set") != null) {
 339             ParseNode set = pn.getChild("set");
 340             Expr expr = parse_expr(set.getChild("expr"));
 341
 342             if (expr == null) {
 343                 return null;
 344             }
 345
 346             String setname = set.getChild("name").getTerminal();
 347             assert setname != null;
 348             SetDescriptor sd = lookupSet(setname);
 349
 350             if (sd == null) {
 351                 er.report(set.getChild("name"), "Undefined set '" + setname + "'");
 352                 return null;
 353             }
 354
 355             return new SetInclusion(expr, sd);
 356         } else if (pn.getChild("relation") != null) {
 357             ParseNode relation = pn.getChild("relation");
 358             Expr leftexpr = parse_expr(relation.getChild("left").getChild("expr"));
 359             Expr rightexpr = parse_expr(relation.getChild("right").getChild("expr"));
 360
 361             if ((leftexpr == null) || (rightexpr == null)) {
 362                 return null;
 363             }
 364
 365             String relname = relation.getChild("name").getTerminal();
 366             assert relname != null;
 367             RelationDescriptor rd = lookupRelation(relname);
 368
 369             if (rd == null) {
 370                 er.report(relation.getChild("name"), "Undefined relation '" + relname + "'");
 371                 return null;
 372             }
 373
 374             return new RelationInclusion(leftexpr, rightexpr, rd);
 375         } else {
 376             throw new IRException();
 377         }
 378     }
 379
 380     private boolean parse_constraints(ParseNode pn) {
 381         if (!precheck(pn, "constraints")) {
 382             return false;
 383         }
 384         //System.out.println(pn.PPrint(2,true));
 385
 386         boolean ok = true;
 387         ParseNodeVector constraints = pn.getChildren();
 388
 389         for (int i = 0; i < constraints.size(); i++) {
 390             ParseNode constraint = constraints.elementAt(i);
 391             assert constraint.getLabel().equals("constraint");
 392             if (!parse_constraint(constraint)) {
 393                 ok = false;
 394             }
 395         }
 396
 397         /* do any post checks... (type constraints, etc?) */
 398
 399         Iterator consiterator = state.vConstraints.iterator();
 400
 401         while (consiterator.hasNext()) {
 402             Constraint cons = (Constraint) consiterator.next();
 403
 404             final SymbolTable consst = cons.getSymbolTable();
 405             SemanticAnalyzer sa = new SemanticAnalyzer() {
 406                     public IRErrorReporter getErrorReporter() { return er; }
 407                     public SymbolTable getSymbolTable() { return consst; }
 408                 };
 409
 410             TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
 411
 412             if (constype == null) {
 413                 System.out.println("Failed attempting to type constraint");
 414                 ok = false;
 415             } else if (constype != ReservedTypeDescriptor.INT) {
 416                 er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
 417                 ok = false;
 418             }
 419         }
 420
 421         return ok;
 422     }
 423
 424     private boolean parse_constraint(ParseNode pn) {
 425         if (!precheck(pn, "constraint")) {
 426             return false;
 427         }
 428
 429         boolean ok = true;
 430         Constraint constraint = new Constraint();
 431
 432         /* test crash */
 433         boolean crash = pn.getChild("crash") != null;
 434         constraint.setCrash(crash);
 435
 436         /* set up symbol table for constraint */
 437         assert sts.empty();
 438         sts.push(constraint.getSymbolTable());
 439
 440         /* get quantifiers */
 441         if (pn.getChild("quantifiers") != null) {
 442             ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
 443
 444             for (int i = 0; i < quantifiers.size(); i++) {
 445                 ParseNode qn = quantifiers.elementAt(i);
 446                 assert qn.getLabel().equals("quantifier");
 447                 Quantifier quantifier = parse_quantifier(qn);
 448                 if (quantifier == null) {
 449                     System.out.println("Failed parsing quantifier");
 450                     ok = false;
 451                 } else {
 452                     constraint.addQuantifier(quantifier);
 453                 }
 454             }
 455         }
 456
 457         /* get body */
 458         LogicStatement logicexpr = parse_body(pn.getChild("body"));
 459
 460         if (logicexpr == null) {
 461             System.out.println("Failed parsing logical expression");
 462             ok = false;
 463         } else {
 464             constraint.setLogicStatement(logicexpr);
 465         }
 466
 467         /* pop symbol table stack */
 468         SymbolTable st = sts.pop();
 469
 470         /* make sure the stack we pop is our constraint s.t. */
 471         assert st == constraint.getSymbolTable();
 472         assert sts.empty();
 473
 474         /* add to vConstraints */
 475         vConstraints.addElement(constraint);
 476
 477         return ok;
 478     }
 479
 480     private Quantifier parse_quantifier(ParseNode pn) {
 481         if (!precheck(pn, "quantifier")) {
 482             return null;
 483         }
 484
 485         if (pn.getChild("forall") != null) { /* forall element in Set */
 486             SetQuantifier sq = new SetQuantifier();
 487
 488             /* get var */
 489             VarDescriptor vd = reserveName(pn.getChild("var"));
 490
 491             if (vd == null) {
 492                 return null;
 493             }
 494
 495             sq.setVar(vd);
 496
 497             /* parse the set */
 498             SetDescriptor set = parse_set(pn.getChild("set"));
 499             assert set != null;
 500             sq.setSet(set);
 501             vd.setSet(set);
 502
 503             vd.setType(set.getType());
 504
 505             /* return to caller */
 506             return sq;
 507
 508         } else if (pn.getChild("relation") != null) { /* for < v1, v2 > in Relation */
 509             RelationQuantifier rq = new RelationQuantifier();
 510
 511             /* get vars */
 512             VarDescriptor vd1 = reserveName(pn.getChild("left"));
 513             VarDescriptor vd2 = reserveName(pn.getChild("right"));
 514
 515             if ((vd1 == null) || (vd2 == null)) {
 516                 return null;
 517             }
 518
 519             rq.setTuple(vd1, vd2);
 520
 521             /* get relation */
 522             String relationname = pn.getChild("relation").getTerminal();
 523             assert relationname != null;
 524             RelationDescriptor rd = lookupRelation(relationname);
 525
 526             if (rd == null) {
 527                 return null;
 528             }
 529
 530             rq.setRelation(rd);
 531             vd1.setType(rd.getDomain().getType());
 532             vd1.setSet(rd.getDomain());
 533             vd2.setType(rd.getRange().getType());
 534             vd2.setSet(rd.getRange());
 535             return rq;
 536         } else if (pn.getChild("for") != null) { /* for j = x to y */
 537             ForQuantifier fq = new ForQuantifier();
 538
 539             /* grab var */
 540             VarDescriptor vd = reserveName(pn.getChild("var"));
 541
 542             if (vd == null) {
 543                 return null;
 544             }
 545
 546             vd.setSet(lookupSet("int", false));
 547             vd.setType(ReservedTypeDescriptor.INT);
 548             fq.setVar(vd);
 549
 550             /* grab lower/upper bounds */
 551             Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
 552             Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
 553
 554
 555             if ((lower == null) || (upper == null)) {
 556                 return null;
 557             }
 558             vd.setBounds(lower,upper);
 559             fq.setBounds(lower, upper);
 560
 561             return fq;
 562         } else {
 563             throw new IRException("not supported yet");
 564         }
 565     }
 566
 567     private LogicStatement parse_body(ParseNode pn) {
 568         if (!precheck(pn, "body")) {
 569             return null;
 570         }
 571
 572         if (pn.getChild("and") != null) {
 573             /* body AND body */
 574             LogicStatement left, right;
 575             left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
 576             right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
 577
 578             if ((left == null) || (right == null)) {
 579                 return null;
 580             }
 581
 582             // what do we want to call the and/or/not body classes?
 583             return new LogicStatement(LogicStatement.AND, left, right);
 584         } else if (pn.getChild("or") != null) {
 585             /* body OR body */
 586             LogicStatement left, right;
 587             left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
 588             right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
 589
 590             if ((left == null) || (right == null)) {
 591                 return null;
 592             }
 593
 594             return new LogicStatement(LogicStatement.OR, left, right);
 595         } else if (pn.getChild("not") != null) {
 596             /* NOT body */
 597             LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
 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("sumexpr") != null) {
1269             return parse_sum(pn.getChild("sumexpr"));
1270         } else if (pn.getChild("literal") != null) {
1271             return parse_literal(pn.getChild("literal"));
1272         } else if (pn.getChild("operator") != null) {
1273             return parse_operator(pn.getChild("operator"));
1274         } else if (pn.getChild("relation") != null) {
1275             return parse_relation(pn.getChild("relation"));
1276         } else if (pn.getChild("sizeof") != null) {
1277             return parse_sizeof(pn.getChild("sizeof"));
1278         } else if (pn.getChild("simple_expr") != null) {
1279             return parse_simple_expr(pn.getChild("simple_expr"));
1280         } else if (pn.getChild("elementof") != null) {
1281             return parse_elementof(pn.getChild("elementof"));
1282         } else if (pn.getChild("tupleof") != null) {
1283             return parse_tupleof(pn.getChild("tupleof"));
1284         } else if (pn.getChild("isvalid") != null) {
1285             er.report(pn, "Operation 'isvalid' is currently unsupported.");
1286             return null;
1287         } else {
1288             er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1289             return null;
1290         }
1291     }
1292
1293     private Expr parse_elementof(ParseNode pn) {
1294         if (!precheck(pn, "elementof")) {
1295             return null;
1296         }
1297
1298         /* get setname */
1299         String setname = pn.getChild("name").getTerminal();
1300         assert setname != null;
1301         SetDescriptor sd = lookupSet(setname);
1302
1303         if (sd == null) {
1304             er.report(pn, "Undefined set '" + setname + "'");
1305             return null;
1306         }
1307
1308         /* get left side expr */
1309         Expr expr = parse_expr(pn.getChild("expr"));
1310
1311         if (expr == null) {
1312             return null;
1313         }
1314
1315         return new ElementOfExpr(expr, sd);
1316     }
1317
1318     private Expr parse_tupleof(ParseNode pn) {
1319         if (!precheck(pn, "tupleof")) {
1320             return null;
1321         }
1322
1323         /* get relation */
1324         String relname = pn.getChild("name").getTerminal();
1325         assert relname != null;
1326         RelationDescriptor rd = lookupRelation(relname);
1327
1328         if (rd == null) {
1329             er.report(pn, "Undefined relation '" + relname + "'");
1330             return null;
1331         }
1332
1333         Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1334         Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1335
1336         if ((left == null) || (right == null)) {
1337             return null;
1338         }
1339
1340         return new TupleOfExpr(left, right, rd);
1341     }
1342
1343     private Expr parse_simple_expr(ParseNode pn) {
1344         if (!precheck(pn, "simple_expr")) {
1345             return null;
1346         }
1347
1348         // only locations so far
1349         return parse_location(pn.getChild("location"));
1350     }
1351
1352     private Expr parse_location(ParseNode pn) {
1353         if (!precheck(pn, "location")) {
1354             return null;
1355         }
1356
1357         if (pn.getChild("var") != null) {
1358             // should be changed into a namespace check */
1359             return new VarExpr(pn.getChild("var").getTerminal());
1360         } else if (pn.getChild("cast") != null) {
1361             return parse_cast(pn.getChild("cast"));
1362         } else if (pn.getChild("dot") != null) {
1363             return parse_dot(pn.getChild("dot"));
1364         } else {
1365             throw new IRException();
1366         }
1367     }
1368
1369     private RelationExpr parse_relation(ParseNode pn) {
1370         if (!precheck(pn, "relation")) {
1371             return null;
1372         }
1373
1374         String relname = pn.getChild("name").getTerminal();
1375         boolean inverse = pn.getChild("inv") != null;
1376         Expr expr = parse_expr(pn.getChild("expr"));
1377
1378         if (expr == null) {
1379             return null;
1380         }
1381
1382         RelationDescriptor relation = lookupRelation(relname);
1383
1384         if (relation == null) {
1385             /* Semantic Error: relation not definied" */
1386             er.report(pn, "Undefined relation '" + relname + "'");
1387             return null;
1388         }
1389
1390         /* add usage so correct sets are created */
1391         relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1392
1393         return new RelationExpr(expr, relation, inverse);
1394     }
1395
1396     private SizeofExpr parse_sizeof(ParseNode pn) {
1397         if (!precheck(pn, "sizeof")) {
1398             return null;
1399         }
1400
1401         /* get setexpr */
1402         SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1403
1404         if (setexpr == null) {
1405             return null;
1406         }
1407
1408         return new SizeofExpr(setexpr);
1409     }
1410
1411     private SumExpr parse_sum(ParseNode pn) {
1412         if (!precheck(pn, "sumexpr")) {
1413             return null;
1414         }
1415         String setname = pn.getChild("dot").getChild("set").getTerminal();
1416         assert setname != null;
1417         SetDescriptor sd = lookupSet(setname);
1418
1419         if (sd == null) {
1420             er.report(pn, "Unknown or undefined set '" + setname + "'");
1421             return null;
1422         }
1423
1424         RelationDescriptor rd = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1425         rd.addUsage(RelationDescriptor.IMAGE);
1426
1427         return new SumExpr(sd,rd);
1428     }
1429
1430     private CastExpr parse_cast(ParseNode pn) {
1431         if (!precheck(pn, "cast")) {
1432             return null;
1433         }
1434
1435         /* get type */
1436         String typename = pn.getChild("type").getTerminal();
1437         assert typename != null;
1438         TypeDescriptor type = lookupType(typename);
1439
1440         if (type == null) {
1441             /* semantic error: undefined type in cast */
1442             er.report(pn, "Undefined type '" + typename + "' in cast operator");
1443             return null;
1444         }
1445
1446         /* get expr */
1447         Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1448
1449         if (expr == null) {
1450             return null;
1451         }
1452
1453         return new CastExpr(type, expr);
1454     }
1455
1456     private SetExpr parse_setexpr(ParseNode pn) {
1457         if (!precheck(pn, "setexpr")) {
1458             return null;
1459         }
1460
1461         // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1462
1463         if (pn.getChild("set") != null) {
1464             String setname = pn.getChild("set").getTerminal();
1465             assert setname != null;
1466             SetDescriptor sd = lookupSet(setname);
1467
1468             if (sd == null) {
1469                 er.report(pn, "Unknown or undefined set '" + setname + "'");
1470                 return null;
1471             } else {
1472                 return new SetExpr(sd);
1473             }
1474         } else if (pn.getChild("dot") != null) {
1475             VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1476             RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1477             relation.addUsage(RelationDescriptor.IMAGE);
1478             return new ImageSetExpr(vd, relation);
1479         } else if (pn.getChild("dotinv") != null) {
1480             VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1481             RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1482             relation.addUsage(RelationDescriptor.INVIMAGE);
1483             return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1484         } else if (pn.getChild("dotset") != null) {
1485             ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotset").getChild("setexpr"));
1486             RelationDescriptor relation = lookupRelation(pn.getChild("dotset").getChild("relation").getTerminal());
1487             relation.addUsage(RelationDescriptor.IMAGE);
1488             return new ImageSetExpr(ise, relation);
1489         } else if (pn.getChild("dotinvset") != null) {
1490             ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotinvset").getChild("setexpr"));
1491             RelationDescriptor relation = lookupRelation(pn.getChild("dotinvset").getChild("relation").getTerminal());
1492             relation.addUsage(RelationDescriptor.INVIMAGE);
1493             return new ImageSetExpr(ImageSetExpr.INVERSE, ise, relation);
1494         } else {
1495             throw new IRException();
1496         }
1497     }
1498
1499     private VarDescriptor parse_quantifiervar(ParseNode pn) {
1500         if (!precheck(pn, "quantifiervar")) {
1501             return null;
1502         }
1503
1504         /* get var */
1505         String varname = pn.getTerminal();
1506         assert varname != null;
1507
1508         /* NOTE: quantifier var's are only found in the constraints and
1509            model definitions... therefore we can do a semantic check here
1510            to make sure that the variables exist in the symbol table */
1511
1512         /* NOTE: its assumed that the symbol table stack is appropriately
1513            set up with the parent quantifier symbol table */
1514         assert !sts.empty();
1515
1516         /* do semantic check and if valid, add it to symbol table
1517            and add it to the quantifier as well */
1518         if (sts.peek().contains(varname)) {
1519             VarDescriptor vdold=(VarDescriptor)sts.peek().get(varname);
1520             return vdold;
1521             /*     Dan was creating a new VarDescriptor...This seems
1522                    like the wrong thing to do.  We'll just lookup the
1523                    other one.
1524                    --------------------------------------------------
1525                    VarDescriptor vd=new VarDescriptor(varname);
1526                    vd.setSet(vdold.getSet()); return vd;*/
1527         } else {
1528             /* Semantic Error: undefined variable */
1529             er.report(pn, "Undefined variable '" + varname + "'");
1530             return null;
1531         }
1532     }
1533
1534     private LiteralExpr parse_literal(ParseNode pn) {
1535         if (!precheck(pn, "literal")) {
1536             return null;
1537         }
1538
1539         if (pn.getChild("boolean") != null) {
1540             if (pn.getChild("boolean").getChild("true") != null) {
1541                 return new BooleanLiteralExpr(true);
1542             } else {
1543                 return new BooleanLiteralExpr(false);
1544             }
1545         } else if (pn.getChild("decimal") != null) {
1546             String integer = pn.getChild("decimal").getTerminal();
1547
1548             /* Check for integer literal overflow */
1549             BigInteger intLitBI = new BigInteger(integer);
1550             BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1551             BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1552             int value;
1553
1554             if (intLitBI.compareTo(intMin) < 0) {
1555                 value = Integer.MIN_VALUE;
1556                 er.warn(pn, "Integer literal overflow");
1557             } else if (intLitBI.compareTo(intMax) > 0) {
1558                 value = Integer.MAX_VALUE;
1559                 er.warn(pn, "Integer literal overflow");
1560             } else {
1561                 /* no truncation needed */
1562                 value = Integer.parseInt(integer);
1563             }
1564
1565             return new IntegerLiteralExpr(value);
1566         } else if (pn.getChild("token") != null) {
1567             return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1568         } else if (pn.getChild("string") != null) {
1569             throw new IRException("string unsupported");
1570         } else if (pn.getChild("char") != null) {
1571             throw new IRException("char unsupported");
1572         } else {
1573             throw new IRException("unknown literal expression type.");
1574         }
1575     }
1576
1577     private OpExpr parse_operator(ParseNode pn) {
1578         if (!precheck(pn, "operator")) {
1579             return null;
1580         }
1581
1582         String opname = pn.getChild("op").getTerminal();
1583         Opcode opcode = Opcode.decodeFromString(opname);
1584
1585         if (opcode == null) {
1586             er.report(pn, "Unsupported operation: " + opname);
1587             return null;
1588         }
1589
1590         Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1591         Expr right = null;
1592
1593         if (pn.getChild("right") != null) {
1594             right = parse_expr(pn.getChild("right").getChild("expr"));
1595         }
1596
1597         if (left == null) {
1598             return null;
1599         }
1600
1601         if (right == null && opcode != Opcode.NOT) {
1602             er.report(pn, "Two arguments required.");
1603             return null;
1604         }
1605
1606         return new OpExpr(opcode, left, right);
1607     }
1608
1609     private DotExpr parse_dot(ParseNode pn) {
1610         if (!precheck(pn, "dot")) {
1611             return null;
1612         }
1613
1614         Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1615
1616         if (left == null) {
1617             return null;
1618         }
1619
1620         String field = pn.getChild("field").getTerminal();
1621
1622         Expr index = null;
1623
1624         if (pn.getChild("index") != null) {
1625             index = parse_expr(pn.getChild("index").getChild("expr"));
1626
1627             if (index == null) {
1628                 return null;
1629             }
1630         }
1631
1632         return new DotExpr(left, field, index);
1633     }
1634
1635 }