4 import java.math.BigInteger;
7 public class SemanticChecker {
9 private static final boolean CREATE_MISSING = true;
19 SymbolTable stRelations;
21 SymbolTable stGlobals;
23 StructureTypeDescriptor dCurrentType;
27 public SemanticChecker () {
33 public boolean check(State state, IRErrorReporter er) {
36 State.currentState = state;
39 throw new IRException("IRBuilder.build: Received null ErrorReporter");
44 if (state.ptStructures == null) {
45 throw new IRException("IRBuilder.build: Received null ParseNode");
48 state.vConstraints = new Vector();
49 vConstraints = state.vConstraints;
51 state.vRules = new Vector();
52 vRules = state.vRules;
54 state.stTypes = new SymbolTable();
55 stTypes = state.stTypes;
57 state.stSets = new SymbolTable();
58 stSets = state.stSets;
60 state.stRelations = new SymbolTable();
61 stRelations = state.stRelations;
63 state.stGlobals = new SymbolTable();
64 stGlobals = state.stGlobals;
66 sts = new SymbolTableStack();
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);
74 stSets.add(new ReservedSetDescriptor("int", ReservedTypeDescriptor.INT));
75 stSets.add(new ReservedSetDescriptor("token", ReservedTypeDescriptor.INT));
79 er.setFilename(state.infile + ".struct");
80 if (!parse_structures(state.ptStructures)) {
83 er.report(null, "Error parsing structs.");
86 er.setFilename(state.infile + ".space");
87 if (!parse_space(state.ptSpace)) {
89 er.report(null, "Error parsing sets and relations.");
92 er.setFilename(state.infile + ".constraints");
93 if (!parse_constraints(state.ptConstraints)) {
95 er.report(null, "Error parsing constraints.");
98 er.setFilename(state.infile + ".model");
99 if (!parse_rules(state.ptModel)) {
101 er.report(null, "Error parsing model definition rules.");
107 /********************** HELPER FUNCTIONS ************************/
110 * special case lookup that returns null if no such type exists
112 private TypeDescriptor lookupType(String typename) {
113 return lookupType(typename, false);
117 * does a look up in the types symbol table. if the type is
118 * not found than a missing type descriptor is returned
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);
134 private VarDescriptor reserveName(ParseNode pn) {
136 String varname = pn.getTerminal();
137 assert varname != null;
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 + "'");
146 VarDescriptor vd = new VarDescriptor(varname);
153 * special case lookup that returns null if no such set exists
155 private SetDescriptor lookupSet(String setname) {
156 return lookupSet(setname, false);
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
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);
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
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);
188 private static int count = 0;
189 private boolean precheck(ParseNode pn, String label) {
191 er.report(pn, "IE: Expected '" + label + "', got null");
196 if (! pn.getLabel().equals(label)) {
197 er.report(pn, "IE: Expected '" + label + "', got '" + pn.getLabel() + "'");
202 if (state.verbose >= 2) {
203 System.err.println("visiting*" + (count++) + ": " + label);
209 /********************* PARSING FUNCTIONS ************************/
211 private boolean parse_rules(ParseNode pn) {
212 if (!precheck(pn, "rules")) {
217 ParseNodeVector rules = pn.getChildren();
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");
228 Iterator ruleiterator = state.vRules.iterator();
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; }
238 TypeDescriptor guardtype = guard.typecheck(sa);
240 if (guardtype == null) {
242 } else if (guardtype != ReservedTypeDescriptor.INT) {
243 er.report(null, "Type of guard must be 'int' not '" + guardtype.getSymbol() + "'");
247 if (!rule.getInclusion().typecheck(sa)) {
248 er.report(null, "Error typechecking rule:"+rule);
252 Iterator quantifiers = rule.quantifiers();
254 while (quantifiers.hasNext()) {
255 Quantifier q = (Quantifier) quantifiers.next();
257 if (q instanceof ForQuantifier && !((ForQuantifier)q).typecheck(sa)) {
263 /* do any post checks ?? */
268 private boolean parse_rule(ParseNode pn) {
269 if (!precheck(pn, "rule")) {
274 Rule rule = new Rule();
277 boolean isstatic = pn.getChild("static") != null;
278 boolean isdelay = pn.getChild("delay") != null;
279 rule.setStatic(isstatic);
280 rule.setDelay(isdelay);
282 /* set up symbol table for constraint */
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);
293 if (quantifier == null) {
296 rule.addQuantifier(quantifier);
302 Expr guard = parse_expr(pn.getChild("expr"));
307 rule.setGuardExpr(guard);
310 /* inclusion constraint */
311 Inclusion inclusion = parse_inclusion(pn.getChild("inclusion"));
313 if (inclusion == null) {
316 rule.setInclusion(inclusion);
319 /* pop symbol table stack */
320 SymbolTable st = sts.pop();
321 sts.pop(); /* pop off globals */
323 /* make sure the stack we pop is our rule s.t. */
324 assert st == rule.getSymbolTable();
327 /* add rule to global set */
328 vRules.addElement(rule);
333 private Inclusion parse_inclusion(ParseNode pn) {
334 if (!precheck(pn, "inclusion")) {
338 if (pn.getChild("set") != null) {
339 ParseNode set = pn.getChild("set");
340 Expr expr = parse_expr(set.getChild("expr"));
346 String setname = set.getChild("name").getTerminal();
347 assert setname != null;
348 SetDescriptor sd = lookupSet(setname);
351 er.report(set.getChild("name"), "Undefined set '" + setname + "'");
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"));
361 if ((leftexpr == null) || (rightexpr == null)) {
365 String relname = relation.getChild("name").getTerminal();
366 assert relname != null;
367 RelationDescriptor rd = lookupRelation(relname);
370 er.report(relation.getChild("name"), "Undefined relation '" + relname + "'");
374 return new RelationInclusion(leftexpr, rightexpr, rd);
376 throw new IRException();
380 private boolean parse_constraints(ParseNode pn) {
381 if (!precheck(pn, "constraints")) {
384 //System.out.println(pn.PPrint(2,true));
387 ParseNodeVector constraints = pn.getChildren();
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)) {
397 /* do any post checks... (type constraints, etc?) */
399 Iterator consiterator = state.vConstraints.iterator();
401 while (consiterator.hasNext()) {
402 Constraint cons = (Constraint) consiterator.next();
404 final SymbolTable consst = cons.getSymbolTable();
405 SemanticAnalyzer sa = new SemanticAnalyzer() {
406 public IRErrorReporter getErrorReporter() { return er; }
407 public SymbolTable getSymbolTable() { return consst; }
410 TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
412 if (constype == null) {
413 System.out.println("Failed attempting to type constraint");
415 } else if (constype != ReservedTypeDescriptor.INT) {
416 er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
424 private boolean parse_constraint(ParseNode pn) {
425 if (!precheck(pn, "constraint")) {
430 Constraint constraint = new Constraint();
433 boolean crash = pn.getChild("crash") != null;
434 constraint.setCrash(crash);
436 /* set up symbol table for constraint */
438 sts.push(constraint.getSymbolTable());
440 /* get quantifiers */
441 if (pn.getChild("quantifiers") != null) {
442 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
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");
452 constraint.addQuantifier(quantifier);
458 LogicStatement logicexpr = parse_body(pn.getChild("body"));
460 if (logicexpr == null) {
461 System.out.println("Failed parsing logical expression");
464 constraint.setLogicStatement(logicexpr);
467 /* pop symbol table stack */
468 SymbolTable st = sts.pop();
470 /* make sure the stack we pop is our constraint s.t. */
471 assert st == constraint.getSymbolTable();
474 /* add to vConstraints */
475 vConstraints.addElement(constraint);
480 private Quantifier parse_quantifier(ParseNode pn) {
481 if (!precheck(pn, "quantifier")) {
485 if (pn.getChild("forall") != null) { /* forall element in Set */
486 SetQuantifier sq = new SetQuantifier();
489 VarDescriptor vd = reserveName(pn.getChild("var"));
498 SetDescriptor set = parse_set(pn.getChild("set"));
503 vd.setType(set.getType());
505 /* return to caller */
508 } else if (pn.getChild("relation") != null) { /* for < v1, v2 > in Relation */
509 RelationQuantifier rq = new RelationQuantifier();
512 VarDescriptor vd1 = reserveName(pn.getChild("left"));
513 VarDescriptor vd2 = reserveName(pn.getChild("right"));
515 if ((vd1 == null) || (vd2 == null)) {
519 rq.setTuple(vd1, vd2);
522 String relationname = pn.getChild("relation").getTerminal();
523 assert relationname != null;
524 RelationDescriptor rd = lookupRelation(relationname);
530 rd.addUsage(RelationDescriptor.IMAGE);
532 vd1.setType(rd.getDomain().getType());
533 vd1.setSet(rd.getDomain());
534 vd2.setType(rd.getRange().getType());
535 vd2.setSet(rd.getRange());
537 } else if (pn.getChild("for") != null) { /* for j = x to y */
538 ForQuantifier fq = new ForQuantifier();
541 VarDescriptor vd = reserveName(pn.getChild("var"));
547 vd.setSet(lookupSet("int", false));
548 vd.setType(ReservedTypeDescriptor.INT);
551 /* grab lower/upper bounds */
552 Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
553 Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
556 if ((lower == null) || (upper == null)) {
559 vd.setBounds(lower,upper);
560 fq.setBounds(lower, upper);
564 throw new IRException("not supported yet");
568 private LogicStatement parse_body(ParseNode pn) {
569 if (!precheck(pn, "body")) {
573 if (pn.getChild("and") != null) {
575 LogicStatement left, right;
576 left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
577 right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
579 if ((left == null) || (right == null)) {
583 // what do we want to call the and/or/not body classes?
584 return new LogicStatement(LogicStatement.AND, left, right);
585 } else if (pn.getChild("or") != null) {
587 LogicStatement left, right;
588 left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
589 right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
591 if ((left == null) || (right == null)) {
595 return new LogicStatement(LogicStatement.OR, left, right);
596 } else if (pn.getChild("not") != null) {
598 LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
603 return new LogicStatement(LogicStatement.NOT, left);
604 } else if (pn.getChild("predicate") != null) {
605 return parse_predicate(pn.getChild("predicate"));
607 throw new IRException();
611 private Predicate parse_predicate(ParseNode pn) {
612 if (!precheck(pn, "predicate")) {
616 if (pn.getChild("inclusion") != null) {
617 ParseNode in = pn.getChild("inclusion");
620 Expr expr = parse_expr(in.getChild("expr"));
627 SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
629 if (setexpr == null) {
633 return new InclusionPredicate(expr, setexpr);
634 } else if (pn.getChild("expr") != null) {
635 Expr expr = parse_expr(pn.getChild("expr"));
641 return new ExprPredicate(expr);
643 throw new IRException();
647 private SetDescriptor parse_set(ParseNode pn) {
648 if (!precheck(pn, "set")) {
652 if (pn.getChild("name") != null) {
653 String setname = pn.getChild("name").getTerminal();
654 assert setname != null;
656 if (!stSets.contains(setname)) {
657 /* Semantic Error: unknown set */
658 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
661 /* all good, get setdescriptor */
662 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
666 } else if (pn.getChild("listofliterals") != null) {
667 TokenSetDescriptor tokenset = new TokenSetDescriptor();
668 ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
669 assert token_literals.size() > 0;
671 for (int i = 0; i < token_literals.size(); i++) {
672 ParseNode literal = token_literals.elementAt(i);
673 assert literal.getLabel().equals("literal");
674 LiteralExpr litexpr = parse_literal(literal);
676 if (litexpr == null) {
680 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
681 tokenset.addLiteral(litexpr);
683 er.report(literal, "Elements of a user-defined set must be of type token or integer");
684 // return null; /* don't think we need to return null */
690 throw new IRException(pn.getTerminal());
694 private boolean parse_space(ParseNode pn) {
695 if (!precheck(pn, "space")) {
700 ParseNodeVector sets = pn.getChildren("setdefinition");
701 ParseNodeVector relations = pn.getChildren("relationdefinition");
703 assert pn.getChildren().size() == (sets.size() + relations.size());
706 for (int i = 0; i < sets.size(); i++) {
707 if (!parse_setdefinition(sets.elementAt(i))) {
712 /* parse relations */
713 for (int i = 0; i < relations.size(); i++) {
714 if (!parse_relationdefinition(relations.elementAt(i))) {
719 // ok, all the spaces have been parsed, now we should typecheck and check
722 // #TBD#: typecheck and check for cycles
724 /* replace missing with actual */
725 Iterator allsets = state.stSets.descriptors();
727 while (allsets.hasNext()) {
728 SetDescriptor sd = (SetDescriptor) allsets.next();
729 Vector subsets = sd.getSubsets();
731 for (int i = 0; i < subsets.size(); i++) {
732 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
734 if (subset instanceof MissingSetDescriptor) {
735 SetDescriptor newsubset = lookupSet(subset.getSymbol());
737 if (newsubset == null) {
738 er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
740 subsets.setElementAt(newsubset, i);
749 private boolean parse_setdefinition(ParseNode pn) {
750 if (!precheck(pn, "setdefinition")) {
757 String setname = pn.getChild("name").getTerminal();
758 assert (setname != null);
760 SetDescriptor sd = new SetDescriptor(setname);
763 String settype = pn.getChild("type").getTerminal();
764 TypeDescriptor type = lookupType(settype);
766 er.report(pn, "Undefined type '" + settype + "'");
772 /* is this a partition? */
773 boolean partition = pn.getChild("partition") != null;
774 sd.isPartition(partition);
776 /* if set has subsets, add them to set descriptor */
777 if (pn.getChild("setlist") != null) {
778 ParseNodeVector setlist = pn.getChild("setlist").getChildren();
780 for (int i = 0; i < setlist.size(); i++) {
781 String subsetname = setlist.elementAt(i).getLabel();
782 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
786 /* add set to symbol table */
787 if (stSets.contains(setname)) {
788 // Semantic Check: redefinition
789 er.report(pn, "Redefinition of set: " + setname);
798 private boolean parse_relationdefinition(ParseNode pn) {
799 if (!precheck(pn, "relationdefinition")) {
805 /* get relation name */
806 String relname = pn.getChild("name").getTerminal();
807 assert relname != null;
809 RelationDescriptor rd = new RelationDescriptor(relname);
811 /* check if static */
812 boolean bStatic = pn.getChild("static") != null;
813 rd.isStatic(bStatic);
816 String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
817 assert domainsetname != null;
820 String rangesetname = pn.getChild("range").getChild("type").getTerminal();
821 assert rangesetname != null;
823 /* get domain multiplicity */
825 if (pn.getChild("domain").getChild("domainmult") != null)
826 domainmult = pn.getChild("domain").getChild("domainmult").getChild("mult").getTerminal();
827 //assert domainmult != null;
829 /* get range multiplicity */
831 if (pn.getChild("range").getChild("domainrange") != null)
832 rangemult = pn.getChild("range").getChild("domainrange").getChild("mult").getTerminal();
833 //assert rangemult != null;
835 /* NOTE: it is assumed that the sets have been parsed already so that the
836 set namespace is fully populated. any missing setdescriptors for the set
837 symbol table will be assumed to be errors and reported. */
839 SetDescriptor domainset = lookupSet(domainsetname);
840 if (domainset == null) {
841 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
844 rd.setDomain(domainset);
847 SetDescriptor rangeset = lookupSet(rangesetname);
848 if (rangeset == null) {
849 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
852 rd.setRange(rangeset);
855 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
857 /* lets add the relation to the global symbol table */
858 if (!stRelations.contains(relname)) {
861 er.report(pn, "Redefinition of relation '" + relname + "'");
868 private boolean parse_structures(ParseNode pn) {
869 if (!precheck(pn, "structures")) {
874 ParseNodeVector structures = pn.getChildren("structure");
876 for (int i = 0; i < structures.size(); i++) {
877 if (!parse_structure(structures.elementAt(i))) {
882 ParseNodeVector globals = pn.getChildren("global");
884 for (int i = 0; i < globals.size(); i++) {
885 if (!parse_global(globals.elementAt(i))) {
890 // ok, all the structures have been parsed, now we gotta type check
892 Enumeration types = stTypes.getDescriptors();
893 while (types.hasMoreElements()) {
894 TypeDescriptor t = (TypeDescriptor) types.nextElement();
896 if (t instanceof ReservedTypeDescriptor) {
897 // we don't need to check reserved types
898 } else if (t instanceof StructureTypeDescriptor) {
900 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
901 TypeDescriptor subtype = type.getSuperType();
903 // check that the subtype is valid
904 if (subtype instanceof MissingTypeDescriptor) {
905 TypeDescriptor newtype = lookupType(subtype.getSymbol());
906 if (newtype == null) {
907 // subtype not defined anywheere
908 // #TBD#: somehow determine how we can get the original parsenode (global function?)
909 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
912 type.setSuperType(newtype);
916 Iterator fields = type.getFields();
918 while (fields.hasNext()) {
919 FieldDescriptor field = (FieldDescriptor) fields.next();
920 TypeDescriptor fieldtype = field.getType();
922 assert fieldtype != null;
924 // check that the type is valid
925 if (fieldtype instanceof MissingTypeDescriptor) {
926 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
927 if (newtype == null) {
928 // type never defined
929 // #TBD#: replace new ParseNode with original parsenode
931 if (!field.getPtr()) {
932 /* Pointer types don't have to be defined */
933 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
937 assert newtype != null;
938 field.setType(newtype);
943 Iterator labels = type.getLabels();
945 while (labels.hasNext()) {
946 LabelDescriptor label = (LabelDescriptor) labels.next();
947 TypeDescriptor labeltype = label.getType();
949 assert labeltype != null;
951 // check that the type is valid
952 if (labeltype instanceof MissingTypeDescriptor) {
953 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
954 if (newtype == null) {
955 // type never defined
956 // #TBD#: replace new ParseNode with original parsenode
957 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
960 assert newtype != null;
961 label.setType(newtype);
967 throw new IRException("shouldn't be any other typedescriptor classes");
975 types = stTypes.getDescriptors();
977 while (types.hasMoreElements()) {
978 TypeDescriptor t = (TypeDescriptor) types.nextElement();
980 if (t instanceof ReservedTypeDescriptor) {
981 // we don't need to check reserved types
982 } else if (t instanceof StructureTypeDescriptor) {
984 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
985 TypeDescriptor subtype = type.getSuperType();
986 Iterator fields = type.getFields();
988 while (fields.hasNext()) {
989 FieldDescriptor field = (FieldDescriptor) fields.next();
991 if (field instanceof ArrayDescriptor) {
992 ArrayDescriptor ad = (ArrayDescriptor) field;
993 Expr indexbound = ad.getIndexBound();
994 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
995 public IRErrorReporter getErrorReporter() { return er; }
996 public SymbolTable getSymbolTable() { return stGlobals; }
999 if (indextype == null) {
1001 } else if (indextype != ReservedTypeDescriptor.INT) {
1002 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
1008 Iterator labels = type.getLabels();
1010 while (labels.hasNext()) {
1011 LabelDescriptor label = (LabelDescriptor) labels.next();
1012 Expr index = label.getIndex();
1014 if (index != null) {
1015 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
1016 public IRErrorReporter getErrorReporter() { return er; }
1017 public SymbolTable getSymbolTable() { return stGlobals; }
1020 if (indextype != ReservedTypeDescriptor.INT) {
1021 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
1027 throw new IRException("shouldn't be any other typedescriptor classes");
1031 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
1032 // subtypes, of course, are not real subtypes, they are merely a way to validate a
1038 private boolean parse_global(ParseNode pn) {
1039 if (!precheck(pn, "global")) {
1043 String name = pn.getChild("name").getTerminal();
1044 assert name != null;
1046 String type = pn.getChild("type").getTerminal();
1047 assert type != null;
1049 TypeDescriptor td = lookupType(type);
1052 if (stGlobals.contains(name)) {
1053 /* redefinition of global */
1054 er.report(pn, "Redefinition of global '" + name + "'");
1058 stGlobals.add(new VarDescriptor(name, name, td,true));
1062 private boolean parse_structure(ParseNode pn) {
1063 if (!precheck(pn, "structure")) {
1068 String typename = pn.getChild("name").getTerminal();
1069 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1071 if (pn.getChild("subtype") != null) {
1072 // has a subtype, lets try to resolve it
1073 String subtype = pn.getChild("subtype").getTerminal();
1075 if (subtype.equals(typename)) {
1076 // Semantic Error: cyclic inheritance
1077 er.report(pn, "Cyclic inheritance prohibited");
1081 /* lookup the type to get the type descriptor */
1082 type.setSuperType(lookupType(subtype, CREATE_MISSING));
1083 } else if (pn.getChild("subclass") != null) {
1084 // has a subtype, lets try to resolve it
1085 String subclass = pn.getChild("subclass").getTerminal();
1087 if (subclass.equals(typename)) {
1088 // Semantic Error: cyclic inheritance
1089 er.report(pn, "Cyclic inheritance prohibited");
1093 /* lookup the type to get the type descriptor */
1094 type.setSuperType(lookupType(subclass, CREATE_MISSING));
1095 type.setSubClass(true);
1098 // set the current type so that the recursive parses on the labels
1099 // and fields can add themselves automatically to the current type
1100 dCurrentType = type;
1102 // parse the labels and fields
1103 if (pn.getChild("lf")!=null && !parse_labelsandfields(pn.getChild("lf"))) {
1107 if (stTypes.contains(typename)) {
1108 er.report(pn, "Redefinition of type '" + typename + "'");
1117 private boolean parse_labelsandfields(ParseNode pn) {
1118 if (!precheck(pn, "lf")) {
1124 // check the fields first (need the field names
1125 // to type check the labels)
1126 if (!parse_fields(pn.getChild("fields"))) {
1130 // check the labels now that all the fields are sorted
1131 if (!parse_labels(pn.getChild("labels"))) {
1138 private boolean parse_fields(ParseNode pn) {
1139 if (!precheck(pn, "fields")) {
1145 /* NOTE: because the order of the fields is important when defining a data structure,
1146 and because the order is defined by the order of the fields defined in the field
1147 vector, its important that the parser returns the fields in the correct order */
1149 ParseNodeVector fields = pn.getChildren();
1151 for (int i = 0; i < fields.size(); i++) {
1152 ParseNode field = fields.elementAt(i);
1157 if (field.getChild("reserved") != null) {
1159 // #TBD#: it will be necessary for reserved field descriptors to generate
1160 // a unique symbol for the type descriptor requires it for its hashtable
1161 fd = new ReservedFieldDescriptor();
1164 name = field.getChild("name").getTerminal();
1165 fd = new FieldDescriptor(name);
1169 String type = field.getChild("type").getTerminal();
1170 boolean ptr = field.getChild("*") != null;
1173 fd.setType(lookupType(type, CREATE_MISSING));
1175 if (field.getChild("index") != null) {
1176 // field is an array, so create an array descriptor to wrap the
1177 // field descriptor and then replace the top level field descriptor with
1178 // this array descriptor
1179 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1181 // #ATTN#: do we really want to return an exception here?
1182 throw new IRException("invalid index expression");
1184 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1188 // add the current field to the current type
1189 if (reserved == false) {
1190 // lets double check that we are redefining a field
1191 if (dCurrentType.getField(name) != null) {
1192 // Semantic Error: field redefinition
1193 er.report(pn, "Redefinition of field '" + name + "'");
1196 dCurrentType.addField(fd);
1199 dCurrentType.addField(fd);
1206 private boolean parse_labels(ParseNode pn) {
1207 if (!precheck(pn, "labels")) {
1213 /* NOTE: parse_labels should be called after the fields have been parsed because any
1214 labels not found in the field set of the current type will be flagged as errors */
1216 ParseNodeVector labels = pn.getChildren();
1218 for (int i = 0; i < labels.size(); i++) {
1219 ParseNode label = labels.elementAt(i);
1220 String name = label.getChild("name").getTerminal();
1221 LabelDescriptor ld = new LabelDescriptor(name);
1223 if (label.getChild("index") != null) {
1224 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1226 /* #ATTN#: do we really want to return an exception here? */
1227 throw new IRException("Invalid expression");
1232 String type = label.getChild("type").getTerminal();
1234 ld.setType(lookupType(type, CREATE_MISSING));
1236 String field = label.getChild("field").getTerminal();
1237 FieldDescriptor fd = dCurrentType.getField(field);
1240 /* Semantic Error: Undefined field in label */
1241 er.report(label, "Undefined field '" + field + "' in label");
1247 /* add label to current type */
1248 if (dCurrentType.getLabel(name) != null) {
1249 /* semantic error: label redefinition */
1250 er.report(pn, "Redefinition of label '" + name + "'");
1253 dCurrentType.addLabel(ld);
1260 private Expr parse_expr(ParseNode pn) {
1261 if (!precheck(pn, "expr")) {
1265 if (pn.getChild("var") != null) {
1266 // we've got a variable reference... we'll have to scope check it later
1267 // when we are completely done... there are also some issues of cyclic definitions
1268 return new VarExpr(pn.getChild("var").getTerminal());
1269 } else if (pn.getChild("sumexpr") != null) {
1270 return parse_sum(pn.getChild("sumexpr"));
1271 } else if (pn.getChild("literal") != null) {
1272 return parse_literal(pn.getChild("literal"));
1273 } else if (pn.getChild("operator") != null) {
1274 return parse_operator(pn.getChild("operator"));
1275 } else if (pn.getChild("relation") != null) {
1276 return parse_relation(pn.getChild("relation"));
1277 } else if (pn.getChild("sizeof") != null) {
1278 return parse_sizeof(pn.getChild("sizeof"));
1279 } else if (pn.getChild("simple_expr") != null) {
1280 return parse_simple_expr(pn.getChild("simple_expr"));
1281 } else if (pn.getChild("elementof") != null) {
1282 return parse_elementof(pn.getChild("elementof"));
1283 } else if (pn.getChild("tupleof") != null) {
1284 return parse_tupleof(pn.getChild("tupleof"));
1285 } else if (pn.getChild("isvalid") != null) {
1286 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1289 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1294 private Expr parse_elementof(ParseNode pn) {
1295 if (!precheck(pn, "elementof")) {
1300 String setname = pn.getChild("name").getTerminal();
1301 assert setname != null;
1302 SetDescriptor sd = lookupSet(setname);
1305 er.report(pn, "Undefined set '" + setname + "'");
1309 /* get left side expr */
1310 Expr expr = parse_expr(pn.getChild("expr"));
1316 return new ElementOfExpr(expr, sd);
1319 private Expr parse_tupleof(ParseNode pn) {
1320 if (!precheck(pn, "tupleof")) {
1325 String relname = pn.getChild("name").getTerminal();
1326 assert relname != null;
1327 RelationDescriptor rd = lookupRelation(relname);
1330 er.report(pn, "Undefined relation '" + relname + "'");
1334 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1335 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1337 if ((left == null) || (right == null)) {
1341 return new TupleOfExpr(left, right, rd);
1344 private Expr parse_simple_expr(ParseNode pn) {
1345 if (!precheck(pn, "simple_expr")) {
1349 // only locations so far
1350 return parse_location(pn.getChild("location"));
1353 private Expr parse_location(ParseNode pn) {
1354 if (!precheck(pn, "location")) {
1358 if (pn.getChild("var") != null) {
1359 // should be changed into a namespace check */
1360 return new VarExpr(pn.getChild("var").getTerminal());
1361 } else if (pn.getChild("cast") != null) {
1362 return parse_cast(pn.getChild("cast"));
1363 } else if (pn.getChild("dot") != null) {
1364 return parse_dot(pn.getChild("dot"));
1366 throw new IRException();
1370 private RelationExpr parse_relation(ParseNode pn) {
1371 if (!precheck(pn, "relation")) {
1375 String relname = pn.getChild("name").getTerminal();
1376 boolean inverse = pn.getChild("inv") != null;
1377 Expr expr = parse_expr(pn.getChild("expr"));
1383 RelationDescriptor relation = lookupRelation(relname);
1385 if (relation == null) {
1386 /* Semantic Error: relation not definied" */
1387 er.report(pn, "Undefined relation '" + relname + "'");
1391 /* add usage so correct sets are created */
1392 relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1394 return new RelationExpr(expr, relation, inverse);
1397 private SizeofExpr parse_sizeof(ParseNode pn) {
1398 if (!precheck(pn, "sizeof")) {
1403 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1405 if (setexpr == null) {
1409 return new SizeofExpr(setexpr);
1412 private SumExpr parse_sum(ParseNode pn) {
1413 if (!precheck(pn, "sumexpr")) {
1416 String setname = pn.getChild("dot").getChild("set").getTerminal();
1417 assert setname != null;
1418 SetDescriptor sd = lookupSet(setname);
1421 er.report(pn, "Unknown or undefined set '" + setname + "'");
1425 RelationDescriptor rd = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1426 rd.addUsage(RelationDescriptor.IMAGE);
1428 return new SumExpr(sd,rd);
1431 private CastExpr parse_cast(ParseNode pn) {
1432 if (!precheck(pn, "cast")) {
1437 String typename = pn.getChild("type").getTerminal();
1438 assert typename != null;
1439 TypeDescriptor type = lookupType(typename);
1442 /* semantic error: undefined type in cast */
1443 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1448 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1454 return new CastExpr(type, expr);
1457 private SetExpr parse_setexpr(ParseNode pn) {
1458 if (!precheck(pn, "setexpr")) {
1462 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1464 if (pn.getChild("set") != null) {
1465 String setname = pn.getChild("set").getTerminal();
1466 assert setname != null;
1467 SetDescriptor sd = lookupSet(setname);
1470 er.report(pn, "Unknown or undefined set '" + setname + "'");
1473 return new SetExpr(sd);
1475 } else if (pn.getChild("dot") != null) {
1476 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1477 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1478 relation.addUsage(RelationDescriptor.IMAGE);
1479 return new ImageSetExpr(vd, relation);
1480 } else if (pn.getChild("dotinv") != null) {
1481 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1482 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1483 relation.addUsage(RelationDescriptor.INVIMAGE);
1484 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1485 } else if (pn.getChild("dotset") != null) {
1486 ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotset").getChild("setexpr"));
1487 RelationDescriptor relation = lookupRelation(pn.getChild("dotset").getChild("relation").getTerminal());
1488 relation.addUsage(RelationDescriptor.IMAGE);
1489 return new ImageSetExpr(ise, relation);
1490 } else if (pn.getChild("dotinvset") != null) {
1491 ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotinvset").getChild("setexpr"));
1492 RelationDescriptor relation = lookupRelation(pn.getChild("dotinvset").getChild("relation").getTerminal());
1493 relation.addUsage(RelationDescriptor.INVIMAGE);
1494 return new ImageSetExpr(ImageSetExpr.INVERSE, ise, relation);
1496 throw new IRException();
1500 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1501 if (!precheck(pn, "quantifiervar")) {
1506 String varname = pn.getTerminal();
1507 assert varname != null;
1509 /* NOTE: quantifier var's are only found in the constraints and
1510 model definitions... therefore we can do a semantic check here
1511 to make sure that the variables exist in the symbol table */
1513 /* NOTE: its assumed that the symbol table stack is appropriately
1514 set up with the parent quantifier symbol table */
1515 assert !sts.empty();
1517 /* do semantic check and if valid, add it to symbol table
1518 and add it to the quantifier as well */
1519 if (sts.peek().contains(varname)) {
1520 VarDescriptor vdold=(VarDescriptor)sts.peek().get(varname);
1522 /* Dan was creating a new VarDescriptor...This seems
1523 like the wrong thing to do. We'll just lookup the
1525 --------------------------------------------------
1526 VarDescriptor vd=new VarDescriptor(varname);
1527 vd.setSet(vdold.getSet()); return vd;*/
1529 /* Semantic Error: undefined variable */
1530 er.report(pn, "Undefined variable '" + varname + "'");
1535 private LiteralExpr parse_literal(ParseNode pn) {
1536 if (!precheck(pn, "literal")) {
1540 if (pn.getChild("boolean") != null) {
1541 if (pn.getChild("boolean").getChild("true") != null) {
1542 return new BooleanLiteralExpr(true);
1544 return new BooleanLiteralExpr(false);
1546 } else if (pn.getChild("decimal") != null) {
1547 String integer = pn.getChild("decimal").getTerminal();
1549 /* Check for integer literal overflow */
1550 BigInteger intLitBI = new BigInteger(integer);
1551 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1552 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1555 if (intLitBI.compareTo(intMin) < 0) {
1556 value = Integer.MIN_VALUE;
1557 er.warn(pn, "Integer literal overflow");
1558 } else if (intLitBI.compareTo(intMax) > 0) {
1559 value = Integer.MAX_VALUE;
1560 er.warn(pn, "Integer literal overflow");
1562 /* no truncation needed */
1563 value = Integer.parseInt(integer);
1566 return new IntegerLiteralExpr(value);
1567 } else if (pn.getChild("token") != null) {
1568 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1569 } else if (pn.getChild("string") != null) {
1570 throw new IRException("string unsupported");
1571 } else if (pn.getChild("char") != null) {
1572 throw new IRException("char unsupported");
1574 throw new IRException("unknown literal expression type.");
1578 private OpExpr parse_operator(ParseNode pn) {
1579 if (!precheck(pn, "operator")) {
1583 String opname = pn.getChild("op").getTerminal();
1584 Opcode opcode = Opcode.decodeFromString(opname);
1586 if (opcode == null) {
1587 er.report(pn, "Unsupported operation: " + opname);
1591 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1594 if (pn.getChild("right") != null) {
1595 right = parse_expr(pn.getChild("right").getChild("expr"));
1602 if (right == null && opcode != Opcode.NOT) {
1603 er.report(pn, "Two arguments required.");
1607 return new OpExpr(opcode, left, right);
1610 private DotExpr parse_dot(ParseNode pn) {
1611 if (!precheck(pn, "dot")) {
1615 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1621 String field = pn.getChild("field").getTerminal();
1625 if (pn.getChild("index") != null) {
1626 index = parse_expr(pn.getChild("index").getChild("expr"));
1628 if (index == null) {
1633 return new DotExpr(left, field, index);