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