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")) {
386 ParseNodeVector constraints = pn.getChildren();
388 for (int i = 0; i < constraints.size(); i++) {
389 ParseNode constraint = constraints.elementAt(i);
390 assert constraint.getLabel().equals("constraint");
391 if (!parse_constraint(constraint)) {
396 /* do any post checks... (type constraints, etc?) */
398 Iterator consiterator = state.vConstraints.iterator();
400 while (consiterator.hasNext()) {
401 Constraint cons = (Constraint) consiterator.next();
403 final SymbolTable consst = cons.getSymbolTable();
404 SemanticAnalyzer sa = new SemanticAnalyzer() {
405 public IRErrorReporter getErrorReporter() { return er; }
406 public SymbolTable getSymbolTable() { return consst; }
409 TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
411 if (constype == null) {
412 System.out.println("Failed attempting to type constraint");
414 } else if (constype != ReservedTypeDescriptor.INT) {
415 er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
423 private boolean parse_constraint(ParseNode pn) {
424 if (!precheck(pn, "constraint")) {
429 Constraint constraint = new Constraint();
432 boolean crash = pn.getChild("crash") != null;
433 constraint.setCrash(crash);
435 /* set up symbol table for constraint */
437 sts.push(constraint.getSymbolTable());
439 /* get quantifiers */
440 if (pn.getChild("quantifiers") != null) {
441 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
443 for (int i = 0; i < quantifiers.size(); i++) {
444 ParseNode qn = quantifiers.elementAt(i);
445 assert qn.getLabel().equals("quantifier");
446 Quantifier quantifier = parse_quantifier(qn);
447 if (quantifier == null) {
448 System.out.println("Failed parsing quantifier");
451 constraint.addQuantifier(quantifier);
457 LogicStatement logicexpr = parse_body(pn.getChild("body"));
459 if (logicexpr == null) {
460 System.out.println("Failed parsing logical expression");
463 constraint.setLogicStatement(logicexpr);
466 /* pop symbol table stack */
467 SymbolTable st = sts.pop();
469 /* make sure the stack we pop is our constraint s.t. */
470 assert st == constraint.getSymbolTable();
473 /* add to vConstraints */
474 vConstraints.addElement(constraint);
479 private Quantifier parse_quantifier(ParseNode pn) {
480 if (!precheck(pn, "quantifier")) {
484 if (pn.getChild("forall") != null) { /* forall element in Set */
485 SetQuantifier sq = new SetQuantifier();
488 VarDescriptor vd = reserveName(pn.getChild("var"));
497 SetDescriptor set = parse_set(pn.getChild("set"));
502 vd.setType(set.getType());
504 /* return to caller */
507 } else if (pn.getChild("relation") != null) { /* for < v1, v2 > in Relation */
508 RelationQuantifier rq = new RelationQuantifier();
511 VarDescriptor vd1 = reserveName(pn.getChild("left"));
512 VarDescriptor vd2 = reserveName(pn.getChild("right"));
514 if ((vd1 == null) || (vd2 == null)) {
518 rq.setTuple(vd1, vd2);
521 String relationname = pn.getChild("relation").getTerminal();
522 assert relationname != null;
523 RelationDescriptor rd = lookupRelation(relationname);
530 vd1.setType(rd.getDomain().getType());
531 vd1.setSet(rd.getDomain());
532 vd2.setType(rd.getRange().getType());
533 vd2.setSet(rd.getRange());
535 } else if (pn.getChild("for") != null) { /* for j = x to y */
536 ForQuantifier fq = new ForQuantifier();
539 VarDescriptor vd = reserveName(pn.getChild("var"));
545 vd.setSet(lookupSet("int", false));
546 vd.setType(ReservedTypeDescriptor.INT);
549 /* grab lower/upper bounds */
550 Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
551 Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
554 if ((lower == null) || (upper == null)) {
557 vd.setBounds(lower,upper);
558 fq.setBounds(lower, upper);
562 throw new IRException("not supported yet");
566 private LogicStatement parse_body(ParseNode pn) {
567 if (!precheck(pn, "body")) {
571 if (pn.getChild("and") != null) {
573 LogicStatement left, right;
574 left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
575 right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
577 if ((left == null) || (right == null)) {
581 // what do we want to call the and/or/not body classes?
582 return new LogicStatement(LogicStatement.AND, left, right);
583 } else if (pn.getChild("or") != null) {
585 LogicStatement left, right;
586 left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
587 right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
589 if ((left == null) || (right == null)) {
593 return new LogicStatement(LogicStatement.OR, left, right);
594 } else if (pn.getChild("not") != null) {
596 LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
602 return new LogicStatement(LogicStatement.NOT, left);
603 } else if (pn.getChild("predicate") != null) {
604 return parse_predicate(pn.getChild("predicate"));
606 throw new IRException();
610 private Predicate parse_predicate(ParseNode pn) {
611 if (!precheck(pn, "predicate")) {
615 if (pn.getChild("inclusion") != null) {
616 ParseNode in = pn.getChild("inclusion");
619 Expr expr = parse_expr(in.getChild("expr"));
626 SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
628 if (setexpr == null) {
632 return new InclusionPredicate(expr, setexpr);
633 } else if (pn.getChild("expr") != null) {
634 Expr expr = parse_expr(pn.getChild("expr"));
640 return new ExprPredicate(expr);
642 throw new IRException();
646 private SetDescriptor parse_set(ParseNode pn) {
647 if (!precheck(pn, "set")) {
651 if (pn.getChild("name") != null) {
652 String setname = pn.getChild("name").getTerminal();
653 assert setname != null;
655 if (!stSets.contains(setname)) {
656 /* Semantic Error: unknown set */
657 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
660 /* all good, get setdescriptor */
661 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
665 } else if (pn.getChild("listofliterals") != null) {
666 TokenSetDescriptor tokenset = new TokenSetDescriptor();
667 ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
668 assert token_literals.size() > 0;
670 for (int i = 0; i < token_literals.size(); i++) {
671 ParseNode literal = token_literals.elementAt(i);
672 assert literal.getLabel().equals("literal");
673 LiteralExpr litexpr = parse_literal(literal);
675 if (litexpr == null) {
679 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
680 tokenset.addLiteral(litexpr);
682 er.report(literal, "Elements of a user-defined set must be of type token or integer");
683 // return null; /* don't think we need to return null */
689 throw new IRException(pn.getTerminal());
693 private boolean parse_space(ParseNode pn) {
694 if (!precheck(pn, "space")) {
699 ParseNodeVector sets = pn.getChildren("setdefinition");
700 ParseNodeVector relations = pn.getChildren("relationdefinition");
702 assert pn.getChildren().size() == (sets.size() + relations.size());
705 for (int i = 0; i < sets.size(); i++) {
706 if (!parse_setdefinition(sets.elementAt(i))) {
711 /* parse relations */
712 for (int i = 0; i < relations.size(); i++) {
713 if (!parse_relationdefinition(relations.elementAt(i))) {
718 // ok, all the spaces have been parsed, now we should typecheck and check
721 // #TBD#: typecheck and check for cycles
723 /* replace missing with actual */
724 Iterator allsets = state.stSets.descriptors();
726 while (allsets.hasNext()) {
727 SetDescriptor sd = (SetDescriptor) allsets.next();
728 Vector subsets = sd.getSubsets();
730 for (int i = 0; i < subsets.size(); i++) {
731 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
733 if (subset instanceof MissingSetDescriptor) {
734 SetDescriptor newsubset = lookupSet(subset.getSymbol());
736 if (newsubset == null) {
737 er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
739 subsets.setElementAt(newsubset, i);
748 private boolean parse_setdefinition(ParseNode pn) {
749 if (!precheck(pn, "setdefinition")) {
756 String setname = pn.getChild("name").getTerminal();
757 assert (setname != null);
759 SetDescriptor sd = new SetDescriptor(setname);
762 String settype = pn.getChild("type").getTerminal();
763 TypeDescriptor type = lookupType(settype);
765 er.report(pn, "Undefined type '" + settype + "'");
771 /* is this a partition? */
772 boolean partition = pn.getChild("partition") != null;
773 sd.isPartition(partition);
775 /* if set has subsets, add them to set descriptor */
776 if (pn.getChild("setlist") != null) {
777 ParseNodeVector setlist = pn.getChild("setlist").getChildren();
779 for (int i = 0; i < setlist.size(); i++) {
780 String subsetname = setlist.elementAt(i).getLabel();
781 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
785 /* add set to symbol table */
786 if (stSets.contains(setname)) {
787 // Semantic Check: redefinition
788 er.report(pn, "Redefinition of set: " + setname);
797 private boolean parse_relationdefinition(ParseNode pn) {
798 if (!precheck(pn, "relationdefinition")) {
804 /* get relation name */
805 String relname = pn.getChild("name").getTerminal();
806 assert relname != null;
808 RelationDescriptor rd = new RelationDescriptor(relname);
810 /* check if static */
811 boolean bStatic = pn.getChild("static") != null;
812 rd.isStatic(bStatic);
815 String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
816 assert domainsetname != null;
819 String rangesetname = pn.getChild("range").getChild("type").getTerminal();
820 assert rangesetname != null;
822 /* get domain multiplicity */
824 if (pn.getChild("domain").getChild("domainmult") != null)
825 domainmult = pn.getChild("domain").getChild("domainmult").getChild("mult").getTerminal();
826 //assert domainmult != null;
828 /* get range multiplicity */
830 if (pn.getChild("range").getChild("domainrange") != null)
831 rangemult = pn.getChild("range").getChild("domainrange").getChild("mult").getTerminal();
832 //assert rangemult != null;
834 /* NOTE: it is assumed that the sets have been parsed already so that the
835 set namespace is fully populated. any missing setdescriptors for the set
836 symbol table will be assumed to be errors and reported. */
838 SetDescriptor domainset = lookupSet(domainsetname);
839 if (domainset == null) {
840 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
843 rd.setDomain(domainset);
846 SetDescriptor rangeset = lookupSet(rangesetname);
847 if (rangeset == null) {
848 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
851 rd.setRange(rangeset);
854 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
856 /* lets add the relation to the global symbol table */
857 if (!stRelations.contains(relname)) {
860 er.report(pn, "Redefinition of relation '" + relname + "'");
867 private boolean parse_structures(ParseNode pn) {
868 if (!precheck(pn, "structures")) {
873 ParseNodeVector structures = pn.getChildren("structure");
875 for (int i = 0; i < structures.size(); i++) {
876 if (!parse_structure(structures.elementAt(i))) {
881 ParseNodeVector globals = pn.getChildren("global");
883 for (int i = 0; i < globals.size(); i++) {
884 if (!parse_global(globals.elementAt(i))) {
889 // ok, all the structures have been parsed, now we gotta type check
891 Enumeration types = stTypes.getDescriptors();
892 while (types.hasMoreElements()) {
893 TypeDescriptor t = (TypeDescriptor) types.nextElement();
895 if (t instanceof ReservedTypeDescriptor) {
896 // we don't need to check reserved types
897 } else if (t instanceof StructureTypeDescriptor) {
899 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
900 TypeDescriptor subtype = type.getSuperType();
902 // check that the subtype is valid
903 if (subtype instanceof MissingTypeDescriptor) {
904 TypeDescriptor newtype = lookupType(subtype.getSymbol());
905 if (newtype == null) {
906 // subtype not defined anywheere
907 // #TBD#: somehow determine how we can get the original parsenode (global function?)
908 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
911 type.setSuperType(newtype);
915 Iterator fields = type.getFields();
917 while (fields.hasNext()) {
918 FieldDescriptor field = (FieldDescriptor) fields.next();
919 TypeDescriptor fieldtype = field.getType();
921 assert fieldtype != null;
923 // check that the type is valid
924 if (fieldtype instanceof MissingTypeDescriptor) {
925 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
926 if (newtype == null) {
927 // type never defined
928 // #TBD#: replace new ParseNode with original parsenode
930 if (!field.getPtr()) {
931 /* Pointer types don't have to be defined */
932 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
936 assert newtype != null;
937 field.setType(newtype);
942 Iterator labels = type.getLabels();
944 while (labels.hasNext()) {
945 LabelDescriptor label = (LabelDescriptor) labels.next();
946 TypeDescriptor labeltype = label.getType();
948 assert labeltype != null;
950 // check that the type is valid
951 if (labeltype instanceof MissingTypeDescriptor) {
952 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
953 if (newtype == null) {
954 // type never defined
955 // #TBD#: replace new ParseNode with original parsenode
956 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
959 assert newtype != null;
960 label.setType(newtype);
966 throw new IRException("shouldn't be any other typedescriptor classes");
974 types = stTypes.getDescriptors();
976 while (types.hasMoreElements()) {
977 TypeDescriptor t = (TypeDescriptor) types.nextElement();
979 if (t instanceof ReservedTypeDescriptor) {
980 // we don't need to check reserved types
981 } else if (t instanceof StructureTypeDescriptor) {
983 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
984 TypeDescriptor subtype = type.getSuperType();
985 Iterator fields = type.getFields();
987 while (fields.hasNext()) {
988 FieldDescriptor field = (FieldDescriptor) fields.next();
990 if (field instanceof ArrayDescriptor) {
991 ArrayDescriptor ad = (ArrayDescriptor) field;
992 Expr indexbound = ad.getIndexBound();
993 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
994 public IRErrorReporter getErrorReporter() { return er; }
995 public SymbolTable getSymbolTable() { return stGlobals; }
998 if (indextype == null) {
1000 } else if (indextype != ReservedTypeDescriptor.INT) {
1001 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
1007 Iterator labels = type.getLabels();
1009 while (labels.hasNext()) {
1010 LabelDescriptor label = (LabelDescriptor) labels.next();
1011 Expr index = label.getIndex();
1013 if (index != null) {
1014 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
1015 public IRErrorReporter getErrorReporter() { return er; }
1016 public SymbolTable getSymbolTable() { return stGlobals; }
1019 if (indextype != ReservedTypeDescriptor.INT) {
1020 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
1026 throw new IRException("shouldn't be any other typedescriptor classes");
1030 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
1031 // subtypes, of course, are not real subtypes, they are merely a way to validate a
1037 private boolean parse_global(ParseNode pn) {
1038 if (!precheck(pn, "global")) {
1042 String name = pn.getChild("name").getTerminal();
1043 assert name != null;
1045 String type = pn.getChild("type").getTerminal();
1046 assert type != null;
1048 TypeDescriptor td = lookupType(type);
1051 if (stGlobals.contains(name)) {
1052 /* redefinition of global */
1053 er.report(pn, "Redefinition of global '" + name + "'");
1057 stGlobals.add(new VarDescriptor(name, name, td,true));
1061 private boolean parse_structure(ParseNode pn) {
1062 if (!precheck(pn, "structure")) {
1067 String typename = pn.getChild("name").getTerminal();
1068 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1070 if (pn.getChild("subtype") != null) {
1071 // has a subtype, lets try to resolve it
1072 String subtype = pn.getChild("subtype").getTerminal();
1074 if (subtype.equals(typename)) {
1075 // Semantic Error: cyclic inheritance
1076 er.report(pn, "Cyclic inheritance prohibited");
1080 /* lookup the type to get the type descriptor */
1081 type.setSuperType(lookupType(subtype, CREATE_MISSING));
1082 } else if (pn.getChild("subclass") != null) {
1083 // has a subtype, lets try to resolve it
1084 String subclass = pn.getChild("subclass").getTerminal();
1086 if (subclass.equals(typename)) {
1087 // Semantic Error: cyclic inheritance
1088 er.report(pn, "Cyclic inheritance prohibited");
1092 /* lookup the type to get the type descriptor */
1093 type.setSuperType(lookupType(subclass, CREATE_MISSING));
1094 type.setSubClass(true);
1097 // set the current type so that the recursive parses on the labels
1098 // and fields can add themselves automatically to the current type
1099 dCurrentType = type;
1101 // parse the labels and fields
1102 if (!parse_labelsandfields(pn.getChild("lf"))) {
1106 if (stTypes.contains(typename)) {
1107 er.report(pn, "Redefinition of type '" + typename + "'");
1116 private boolean parse_labelsandfields(ParseNode pn) {
1117 if (!precheck(pn, "lf")) {
1123 // check the fields first (need the field names
1124 // to type check the labels)
1125 if (!parse_fields(pn.getChild("fields"))) {
1129 // check the labels now that all the fields are sorted
1130 if (!parse_labels(pn.getChild("labels"))) {
1137 private boolean parse_fields(ParseNode pn) {
1138 if (!precheck(pn, "fields")) {
1144 /* NOTE: because the order of the fields is important when defining a data structure,
1145 and because the order is defined by the order of the fields defined in the field
1146 vector, its important that the parser returns the fields in the correct order */
1148 ParseNodeVector fields = pn.getChildren();
1150 for (int i = 0; i < fields.size(); i++) {
1151 ParseNode field = fields.elementAt(i);
1156 if (field.getChild("reserved") != null) {
1158 // #TBD#: it will be necessary for reserved field descriptors to generate
1159 // a unique symbol for the type descriptor requires it for its hashtable
1160 fd = new ReservedFieldDescriptor();
1163 name = field.getChild("name").getTerminal();
1164 fd = new FieldDescriptor(name);
1168 String type = field.getChild("type").getTerminal();
1169 boolean ptr = field.getChild("*") != null;
1172 fd.setType(lookupType(type, CREATE_MISSING));
1174 if (field.getChild("index") != null) {
1175 // field is an array, so create an array descriptor to wrap the
1176 // field descriptor and then replace the top level field descriptor with
1177 // this array descriptor
1178 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1180 // #ATTN#: do we really want to return an exception here?
1181 throw new IRException("invalid index expression");
1183 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1187 // add the current field to the current type
1188 if (reserved == false) {
1189 // lets double check that we are redefining a field
1190 if (dCurrentType.getField(name) != null) {
1191 // Semantic Error: field redefinition
1192 er.report(pn, "Redefinition of field '" + name + "'");
1195 dCurrentType.addField(fd);
1198 dCurrentType.addField(fd);
1205 private boolean parse_labels(ParseNode pn) {
1206 if (!precheck(pn, "labels")) {
1212 /* NOTE: parse_labels should be called after the fields have been parsed because any
1213 labels not found in the field set of the current type will be flagged as errors */
1215 ParseNodeVector labels = pn.getChildren();
1217 for (int i = 0; i < labels.size(); i++) {
1218 ParseNode label = labels.elementAt(i);
1219 String name = label.getChild("name").getTerminal();
1220 LabelDescriptor ld = new LabelDescriptor(name);
1222 if (label.getChild("index") != null) {
1223 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1225 /* #ATTN#: do we really want to return an exception here? */
1226 throw new IRException("Invalid expression");
1231 String type = label.getChild("type").getTerminal();
1233 ld.setType(lookupType(type, CREATE_MISSING));
1235 String field = label.getChild("field").getTerminal();
1236 FieldDescriptor fd = dCurrentType.getField(field);
1239 /* Semantic Error: Undefined field in label */
1240 er.report(label, "Undefined field '" + field + "' in label");
1246 /* add label to current type */
1247 if (dCurrentType.getLabel(name) != null) {
1248 /* semantic error: label redefinition */
1249 er.report(pn, "Redefinition of label '" + name + "'");
1252 dCurrentType.addLabel(ld);
1259 private Expr parse_expr(ParseNode pn) {
1260 if (!precheck(pn, "expr")) {
1264 if (pn.getChild("var") != null) {
1265 // we've got a variable reference... we'll have to scope check it later
1266 // when we are completely done... there are also some issues of cyclic definitions
1267 return new VarExpr(pn.getChild("var").getTerminal());
1268 } else if (pn.getChild("literal") != null) {
1269 return parse_literal(pn.getChild("literal"));
1270 } else if (pn.getChild("operator") != null) {
1271 return parse_operator(pn.getChild("operator"));
1272 } else if (pn.getChild("relation") != null) {
1273 return parse_relation(pn.getChild("relation"));
1274 } else if (pn.getChild("sizeof") != null) {
1275 return parse_sizeof(pn.getChild("sizeof"));
1276 } else if (pn.getChild("simple_expr") != null) {
1277 return parse_simple_expr(pn.getChild("simple_expr"));
1278 } else if (pn.getChild("elementof") != null) {
1279 return parse_elementof(pn.getChild("elementof"));
1280 } else if (pn.getChild("tupleof") != null) {
1281 return parse_tupleof(pn.getChild("tupleof"));
1282 } else if (pn.getChild("isvalid") != null) {
1283 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1286 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1291 private Expr parse_elementof(ParseNode pn) {
1292 if (!precheck(pn, "elementof")) {
1297 String setname = pn.getChild("name").getTerminal();
1298 assert setname != null;
1299 SetDescriptor sd = lookupSet(setname);
1302 er.report(pn, "Undefined set '" + setname + "'");
1306 /* get left side expr */
1307 Expr expr = parse_expr(pn.getChild("expr"));
1313 return new ElementOfExpr(expr, sd);
1316 private Expr parse_tupleof(ParseNode pn) {
1317 if (!precheck(pn, "tupleof")) {
1322 String relname = pn.getChild("name").getTerminal();
1323 assert relname != null;
1324 RelationDescriptor rd = lookupRelation(relname);
1327 er.report(pn, "Undefined relation '" + relname + "'");
1331 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1332 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1334 if ((left == null) || (right == null)) {
1338 return new TupleOfExpr(left, right, rd);
1341 private Expr parse_simple_expr(ParseNode pn) {
1342 if (!precheck(pn, "simple_expr")) {
1346 // only locations so far
1347 return parse_location(pn.getChild("location"));
1350 private Expr parse_location(ParseNode pn) {
1351 if (!precheck(pn, "location")) {
1355 if (pn.getChild("var") != null) {
1356 // should be changed into a namespace check */
1357 return new VarExpr(pn.getChild("var").getTerminal());
1358 } else if (pn.getChild("cast") != null) {
1359 return parse_cast(pn.getChild("cast"));
1360 } else if (pn.getChild("dot") != null) {
1361 return parse_dot(pn.getChild("dot"));
1363 throw new IRException();
1367 private RelationExpr parse_relation(ParseNode pn) {
1368 if (!precheck(pn, "relation")) {
1372 String relname = pn.getChild("name").getTerminal();
1373 boolean inverse = pn.getChild("inv") != null;
1374 Expr expr = parse_expr(pn.getChild("expr"));
1380 RelationDescriptor relation = lookupRelation(relname);
1382 if (relation == null) {
1383 /* Semantic Error: relation not definied" */
1384 er.report(pn, "Undefined relation '" + relname + "'");
1388 /* add usage so correct sets are created */
1389 relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1391 return new RelationExpr(expr, relation, inverse);
1394 private SizeofExpr parse_sizeof(ParseNode pn) {
1395 if (!precheck(pn, "sizeof")) {
1400 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1402 if (setexpr == null) {
1406 return new SizeofExpr(setexpr);
1409 private CastExpr parse_cast(ParseNode pn) {
1410 if (!precheck(pn, "cast")) {
1415 String typename = pn.getChild("type").getTerminal();
1416 assert typename != null;
1417 TypeDescriptor type = lookupType(typename);
1420 /* semantic error: undefined type in cast */
1421 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1426 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1432 return new CastExpr(type, expr);
1435 private SetExpr parse_setexpr(ParseNode pn) {
1436 if (!precheck(pn, "setexpr")) {
1440 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1442 if (pn.getChild("set") != null) {
1443 String setname = pn.getChild("set").getTerminal();
1444 assert setname != null;
1445 SetDescriptor sd = lookupSet(setname);
1448 er.report(pn, "Unknown or undefined set '" + setname + "'");
1451 return new SetExpr(sd);
1453 } else if (pn.getChild("dot") != null) {
1454 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1455 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1456 relation.addUsage(RelationDescriptor.IMAGE);
1457 return new ImageSetExpr(vd, relation);
1458 } else if (pn.getChild("dotinv") != null) {
1459 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1460 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1461 relation.addUsage(RelationDescriptor.INVIMAGE);
1462 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1463 } else if (pn.getChild("dotset") != null) {
1464 ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotset").getChild("setexpr"));
1465 RelationDescriptor relation = lookupRelation(pn.getChild("dotset").getChild("relation").getTerminal());
1466 relation.addUsage(RelationDescriptor.IMAGE);
1467 return new ImageSetExpr(ise, relation);
1468 } else if (pn.getChild("dotinvset") != null) {
1469 ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotinvset").getChild("setexpr"));
1470 RelationDescriptor relation = lookupRelation(pn.getChild("dotinvset").getChild("relation").getTerminal());
1471 relation.addUsage(RelationDescriptor.INVIMAGE);
1472 return new ImageSetExpr(ImageSetExpr.INVERSE, ise, relation);
1474 throw new IRException();
1478 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1479 if (!precheck(pn, "quantifiervar")) {
1484 String varname = pn.getTerminal();
1485 assert varname != null;
1487 /* NOTE: quantifier var's are only found in the constraints and
1488 model definitions... therefore we can do a semantic check here
1489 to make sure that the variables exist in the symbol table */
1491 /* NOTE: its assumed that the symbol table stack is appropriately
1492 set up with the parent quantifier symbol table */
1493 assert !sts.empty();
1495 /* do semantic check and if valid, add it to symbol table
1496 and add it to the quantifier as well */
1497 if (sts.peek().contains(varname)) {
1498 VarDescriptor vdold=(VarDescriptor)sts.peek().get(varname);
1500 /* Dan was creating a new VarDescriptor...This seems
1501 like the wrong thing to do. We'll just lookup the
1503 --------------------------------------------------
1504 VarDescriptor vd=new VarDescriptor(varname);
1505 vd.setSet(vdold.getSet()); return vd;*/
1507 /* Semantic Error: undefined variable */
1508 er.report(pn, "Undefined variable '" + varname + "'");
1513 private LiteralExpr parse_literal(ParseNode pn) {
1514 if (!precheck(pn, "literal")) {
1518 if (pn.getChild("boolean") != null) {
1519 if (pn.getChild("boolean").getChild("true") != null) {
1520 return new BooleanLiteralExpr(true);
1522 return new BooleanLiteralExpr(false);
1524 } else if (pn.getChild("decimal") != null) {
1525 String integer = pn.getChild("decimal").getTerminal();
1527 /* Check for integer literal overflow */
1528 BigInteger intLitBI = new BigInteger(integer);
1529 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1530 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1533 if (intLitBI.compareTo(intMin) < 0) {
1534 value = Integer.MIN_VALUE;
1535 er.warn(pn, "Integer literal overflow");
1536 } else if (intLitBI.compareTo(intMax) > 0) {
1537 value = Integer.MAX_VALUE;
1538 er.warn(pn, "Integer literal overflow");
1540 /* no truncation needed */
1541 value = Integer.parseInt(integer);
1544 return new IntegerLiteralExpr(value);
1545 } else if (pn.getChild("token") != null) {
1546 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1547 } else if (pn.getChild("string") != null) {
1548 throw new IRException("string unsupported");
1549 } else if (pn.getChild("char") != null) {
1550 throw new IRException("char unsupported");
1552 throw new IRException("unknown literal expression type.");
1556 private OpExpr parse_operator(ParseNode pn) {
1557 if (!precheck(pn, "operator")) {
1561 String opname = pn.getChild("op").getTerminal();
1562 Opcode opcode = Opcode.decodeFromString(opname);
1564 if (opcode == null) {
1565 er.report(pn, "Unsupported operation: " + opname);
1569 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1572 if (pn.getChild("right") != null) {
1573 right = parse_expr(pn.getChild("right").getChild("expr"));
1580 if (right == null && opcode != Opcode.NOT) {
1581 er.report(pn, "Two arguments required.");
1585 return new OpExpr(opcode, left, right);
1588 private DotExpr parse_dot(ParseNode pn) {
1589 if (!precheck(pn, "dot")) {
1593 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1599 String field = pn.getChild("field").getTerminal();
1603 if (pn.getChild("index") != null) {
1604 index = parse_expr(pn.getChild("index").getChild("expr"));
1606 if (index == null) {
1611 return new DotExpr(left, field, index);