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)) {
84 er.setFilename(state.infile + ".space");
85 if (!parse_space(state.ptSpace)) {
89 er.setFilename(state.infile + ".constraints");
90 if (!parse_constraints(state.ptConstraints)) {
94 er.setFilename(state.infile + ".model");
95 if (!parse_rules(state.ptModel)) {
102 /********************** HELPER FUNCTIONS ************************/
105 * special case lookup that returns null if no such type exists
107 private TypeDescriptor lookupType(String typename) {
108 return lookupType(typename, false);
112 * does a look up in the types symbol table. if the type is
113 * not found than a missing type descriptor is returned
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);
129 private VarDescriptor reserveName(ParseNode pn) {
131 String varname = pn.getTerminal();
132 assert varname != null;
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 + "'");
141 VarDescriptor vd = new VarDescriptor(varname);
148 * special case lookup that returns null if no such set exists
150 private SetDescriptor lookupSet(String setname) {
151 return lookupSet(setname, false);
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
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);
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
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);
183 private static int count = 0;
184 private boolean precheck(ParseNode pn, String label) {
186 er.report(pn, "IE: Expected '" + label + "', got null");
191 if (! pn.getLabel().equals(label)) {
192 er.report(pn, "IE: Expected '" + label + "', got '" + pn.getLabel() + "'");
197 if (state.verbose >= 2) {
198 System.err.println("visiting*" + (count++) + ": " + label);
204 /********************* PARSING FUNCTIONS ************************/
206 private boolean parse_rules(ParseNode pn) {
207 if (!precheck(pn, "rules")) {
212 ParseNodeVector rules = pn.getChildren();
214 for (int i = 0; i < rules.size(); i++) {
215 ParseNode rule = rules.elementAt(i);
216 if (!parse_rule(rule)) {
222 Iterator ruleiterator = state.vRules.iterator();
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; }
232 TypeDescriptor guardtype = guard.typecheck(sa);
234 if (guardtype == null) {
236 } else if (guardtype != ReservedTypeDescriptor.INT) {
237 er.report(null, "Type of guard must be 'int' not '" + guardtype.getSymbol() + "'");
241 if (!rule.getInclusion().typecheck(sa)) {
245 Iterator quantifiers = rule.quantifiers();
247 while (quantifiers.hasNext()) {
248 Quantifier q = (Quantifier) quantifiers.next();
250 if (q instanceof ForQuantifier && !((ForQuantifier)q).typecheck(sa)) {
256 /* do any post checks ?? */
261 private boolean parse_rule(ParseNode pn) {
262 if (!precheck(pn, "rule")) {
267 Rule rule = new Rule();
270 boolean isstatic = pn.getChild("static") != null;
271 boolean isdelay = pn.getChild("delay") != null;
272 rule.setStatic(isstatic);
273 rule.setDelay(isdelay);
275 /* set up symbol table for constraint */
278 sts.push(rule.getSymbolTable());
280 /* optional quantifiers */
281 if (pn.getChild("quantifiers") != null) {
282 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
284 for (int i = 0; i < quantifiers.size(); i++) {
285 ParseNode qn = quantifiers.elementAt(i);
286 Quantifier quantifier = parse_quantifier(qn);
288 if (quantifier == null) {
291 rule.addQuantifier(quantifier);
297 Expr guard = parse_expr(pn.getChild("expr"));
302 rule.setGuardExpr(guard);
305 /* inclusion constraint */
306 Inclusion inclusion = parse_inclusion(pn.getChild("inclusion"));
308 if (inclusion == null) {
311 rule.setInclusion(inclusion);
314 /* pop symbol table stack */
315 SymbolTable st = sts.pop();
316 sts.pop(); /* pop off globals */
318 /* make sure the stack we pop is our rule s.t. */
319 assert st == rule.getSymbolTable();
322 /* add rule to global set */
323 vRules.addElement(rule);
328 private Inclusion parse_inclusion(ParseNode pn) {
329 if (!precheck(pn, "inclusion")) {
333 if (pn.getChild("set") != null) {
334 ParseNode set = pn.getChild("set");
335 Expr expr = parse_expr(set.getChild("expr"));
341 String setname = set.getChild("name").getTerminal();
342 assert setname != null;
343 SetDescriptor sd = lookupSet(setname);
346 er.report(set.getChild("name"), "Undefined set '" + setname + "'");
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"));
356 if ((leftexpr == null) || (rightexpr == null)) {
360 String relname = relation.getChild("name").getTerminal();
361 assert relname != null;
362 RelationDescriptor rd = lookupRelation(relname);
365 er.report(relation.getChild("name"), "Undefined relation '" + relname + "'");
369 return new RelationInclusion(leftexpr, rightexpr, rd);
371 throw new IRException();
375 private boolean parse_constraints(ParseNode pn) {
376 if (!precheck(pn, "constraints")) {
381 ParseNodeVector constraints = pn.getChildren();
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)) {
391 /* do any post checks... (type constraints, etc?) */
393 Iterator consiterator = state.vConstraints.iterator();
395 while (consiterator.hasNext()) {
396 Constraint cons = (Constraint) consiterator.next();
398 final SymbolTable consst = cons.getSymbolTable();
399 SemanticAnalyzer sa = new SemanticAnalyzer() {
400 public IRErrorReporter getErrorReporter() { return er; }
401 public SymbolTable getSymbolTable() { return consst; }
404 TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
406 if (constype == null) {
407 System.out.println("Failed attempting to type constraint");
409 } else if (constype != ReservedTypeDescriptor.INT) {
410 er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
418 private boolean parse_constraint(ParseNode pn) {
419 if (!precheck(pn, "constraint")) {
424 Constraint constraint = new Constraint();
427 boolean crash = pn.getChild("crash") != null;
428 constraint.setCrash(crash);
430 /* set up symbol table for constraint */
432 sts.push(constraint.getSymbolTable());
434 /* get quantifiers */
435 if (pn.getChild("quantifiers") != null) {
436 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
438 for (int i = 0; i < quantifiers.size(); i++) {
439 ParseNode qn = quantifiers.elementAt(i);
440 assert qn.getLabel().equals("quantifier");
441 Quantifier quantifier = parse_quantifier(qn);
442 if (quantifier == null) {
443 System.out.println("Failed parsing quantifier");
446 constraint.addQuantifier(quantifier);
452 LogicStatement logicexpr = parse_body(pn.getChild("body"));
454 if (logicexpr == null) {
455 System.out.println("Failed parsing logical expression");
458 constraint.setLogicStatement(logicexpr);
461 /* pop symbol table stack */
462 SymbolTable st = sts.pop();
464 /* make sure the stack we pop is our constraint s.t. */
465 assert st == constraint.getSymbolTable();
468 /* add to vConstraints */
469 vConstraints.addElement(constraint);
474 private Quantifier parse_quantifier(ParseNode pn) {
475 if (!precheck(pn, "quantifier")) {
479 if (pn.getChild("forall") != null) { /* forall element in Set */
480 SetQuantifier sq = new SetQuantifier();
483 VarDescriptor vd = reserveName(pn.getChild("var"));
492 SetDescriptor set = parse_set(pn.getChild("set"));
497 vd.setType(set.getType());
499 /* return to caller */
502 } else if (pn.getChild("relation") != null) { /* for < v1, v2 > in Relation */
503 RelationQuantifier rq = new RelationQuantifier();
506 VarDescriptor vd1 = reserveName(pn.getChild("left"));
507 VarDescriptor vd2 = reserveName(pn.getChild("right"));
509 if ((vd1 == null) || (vd2 == null)) {
513 rq.setTuple(vd1, vd2);
516 String relationname = pn.getChild("relation").getTerminal();
517 assert relationname != null;
518 RelationDescriptor rd = lookupRelation(relationname);
525 vd1.setType(rd.getDomain().getType());
526 vd1.setSet(rd.getDomain());
527 vd2.setType(rd.getRange().getType());
528 vd2.setSet(rd.getRange());
530 } else if (pn.getChild("for") != null) { /* for j = x to y */
531 ForQuantifier fq = new ForQuantifier();
534 VarDescriptor vd = reserveName(pn.getChild("var"));
540 vd.setSet(lookupSet("int", false));
541 vd.setType(ReservedTypeDescriptor.INT);
544 /* grab lower/upper bounds */
545 Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
546 Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
549 if ((lower == null) || (upper == null)) {
552 vd.setBounds(lower,upper);
553 fq.setBounds(lower, upper);
557 throw new IRException("not supported yet");
561 private LogicStatement parse_body(ParseNode pn) {
562 if (!precheck(pn, "body")) {
566 if (pn.getChild("and") != null) {
568 LogicStatement left, right;
569 left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
570 right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
572 if ((left == null) || (right == null)) {
576 // what do we want to call the and/or/not body classes?
577 return new LogicStatement(LogicStatement.AND, left, right);
578 } else if (pn.getChild("or") != null) {
580 LogicStatement left, right;
581 left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
582 right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
584 if ((left == null) || (right == null)) {
588 return new LogicStatement(LogicStatement.OR, left, right);
589 } else if (pn.getChild("not") != null) {
591 LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
597 return new LogicStatement(LogicStatement.NOT, left);
598 } else if (pn.getChild("predicate") != null) {
599 return parse_predicate(pn.getChild("predicate"));
601 throw new IRException();
605 private Predicate parse_predicate(ParseNode pn) {
606 if (!precheck(pn, "predicate")) {
610 if (pn.getChild("inclusion") != null) {
611 ParseNode in = pn.getChild("inclusion");
614 Expr expr = parse_expr(in.getChild("expr"));
621 SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
623 if (setexpr == null) {
627 return new InclusionPredicate(expr, setexpr);
628 } else if (pn.getChild("expr") != null) {
629 Expr expr = parse_expr(pn.getChild("expr"));
635 return new ExprPredicate(expr);
637 throw new IRException();
641 private SetDescriptor parse_set(ParseNode pn) {
642 if (!precheck(pn, "set")) {
646 if (pn.getChild("name") != null) {
647 String setname = pn.getChild("name").getTerminal();
648 assert setname != null;
650 if (!stSets.contains(setname)) {
651 /* Semantic Error: unknown set */
652 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
655 /* all good, get setdescriptor */
656 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
660 } else if (pn.getChild("listofliterals") != null) {
661 TokenSetDescriptor tokenset = new TokenSetDescriptor();
662 ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
663 assert token_literals.size() > 0;
665 for (int i = 0; i < token_literals.size(); i++) {
666 ParseNode literal = token_literals.elementAt(i);
667 assert literal.getLabel().equals("literal");
668 LiteralExpr litexpr = parse_literal(literal);
670 if (litexpr == null) {
674 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
675 tokenset.addLiteral(litexpr);
677 er.report(literal, "Elements of a user-defined set must be of type token or integer");
678 // return null; /* don't think we need to return null */
684 throw new IRException(pn.getTerminal());
688 private boolean parse_space(ParseNode pn) {
689 if (!precheck(pn, "space")) {
694 ParseNodeVector sets = pn.getChildren("setdefinition");
695 ParseNodeVector relations = pn.getChildren("relationdefinition");
697 assert pn.getChildren().size() == (sets.size() + relations.size());
700 for (int i = 0; i < sets.size(); i++) {
701 if (!parse_setdefinition(sets.elementAt(i))) {
706 /* parse relations */
707 for (int i = 0; i < relations.size(); i++) {
708 if (!parse_relationdefinition(relations.elementAt(i))) {
713 // ok, all the spaces have been parsed, now we should typecheck and check
716 // #TBD#: typecheck and check for cycles
718 /* replace missing with actual */
719 Iterator allsets = state.stSets.descriptors();
721 while (allsets.hasNext()) {
722 SetDescriptor sd = (SetDescriptor) allsets.next();
723 Vector subsets = sd.getSubsets();
725 for (int i = 0; i < subsets.size(); i++) {
726 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
728 if (subset instanceof MissingSetDescriptor) {
729 SetDescriptor newsubset = lookupSet(subset.getSymbol());
731 if (newsubset == null) {
732 er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
734 subsets.setElementAt(newsubset, i);
743 private boolean parse_setdefinition(ParseNode pn) {
744 if (!precheck(pn, "setdefinition")) {
751 String setname = pn.getChild("name").getTerminal();
752 assert (setname != null);
754 SetDescriptor sd = new SetDescriptor(setname);
757 String settype = pn.getChild("type").getTerminal();
758 TypeDescriptor type = lookupType(settype);
760 er.report(pn, "Undefined type '" + settype + "'");
766 /* is this a partition? */
767 boolean partition = pn.getChild("partition") != null;
768 sd.isPartition(partition);
770 /* if set has subsets, add them to set descriptor */
771 if (pn.getChild("setlist") != null) {
772 ParseNodeVector setlist = pn.getChild("setlist").getChildren();
774 for (int i = 0; i < setlist.size(); i++) {
775 String subsetname = setlist.elementAt(i).getLabel();
776 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
780 /* add set to symbol table */
781 if (stSets.contains(setname)) {
782 // Semantic Check: redefinition
783 er.report(pn, "Redefinition of set: " + setname);
792 private boolean parse_relationdefinition(ParseNode pn) {
793 if (!precheck(pn, "relationdefinition")) {
799 /* get relation name */
800 String relname = pn.getChild("name").getTerminal();
801 assert relname != null;
803 RelationDescriptor rd = new RelationDescriptor(relname);
805 /* check if static */
806 boolean bStatic = pn.getChild("static") != null;
807 rd.isStatic(bStatic);
810 String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
811 assert domainsetname != null;
814 String rangesetname = pn.getChild("range").getChild("type").getTerminal();
815 assert rangesetname != null;
817 /* get domain multiplicity */
819 if (pn.getChild("domain").getChild("domainmult") != null)
820 domainmult = pn.getChild("domain").getChild("domainmult").getChild("mult").getTerminal();
821 //assert domainmult != null;
823 /* get range multiplicity */
825 if (pn.getChild("range").getChild("domainrange") != null)
826 rangemult = pn.getChild("range").getChild("domainrange").getChild("mult").getTerminal();
827 //assert rangemult != null;
829 /* NOTE: it is assumed that the sets have been parsed already so that the
830 set namespace is fully populated. any missing setdescriptors for the set
831 symbol table will be assumed to be errors and reported. */
833 SetDescriptor domainset = lookupSet(domainsetname);
834 if (domainset == null) {
835 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
838 rd.setDomain(domainset);
841 SetDescriptor rangeset = lookupSet(rangesetname);
842 if (rangeset == null) {
843 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
846 rd.setRange(rangeset);
849 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
851 /* lets add the relation to the global symbol table */
852 if (!stRelations.contains(relname)) {
855 er.report(pn, "Redefinition of relation '" + relname + "'");
862 private boolean parse_structures(ParseNode pn) {
863 if (!precheck(pn, "structures")) {
868 ParseNodeVector structures = pn.getChildren("structure");
870 for (int i = 0; i < structures.size(); i++) {
871 if (!parse_structure(structures.elementAt(i))) {
876 ParseNodeVector globals = pn.getChildren("global");
878 for (int i = 0; i < globals.size(); i++) {
879 if (!parse_global(globals.elementAt(i))) {
884 // ok, all the structures have been parsed, now we gotta type check
886 Enumeration types = stTypes.getDescriptors();
887 while (types.hasMoreElements()) {
888 TypeDescriptor t = (TypeDescriptor) types.nextElement();
890 if (t instanceof ReservedTypeDescriptor) {
891 // we don't need to check reserved types
892 } else if (t instanceof StructureTypeDescriptor) {
894 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
895 TypeDescriptor subtype = type.getSuperType();
897 // check that the subtype is valid
898 if (subtype instanceof MissingTypeDescriptor) {
899 TypeDescriptor newtype = lookupType(subtype.getSymbol());
900 if (newtype == null) {
901 // subtype not defined anywheere
902 // #TBD#: somehow determine how we can get the original parsenode (global function?)
903 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
906 type.setSuperType(newtype);
910 Iterator fields = type.getFields();
912 while (fields.hasNext()) {
913 FieldDescriptor field = (FieldDescriptor) fields.next();
914 TypeDescriptor fieldtype = field.getType();
916 assert fieldtype != null;
918 // check that the type is valid
919 if (fieldtype instanceof MissingTypeDescriptor) {
920 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
921 if (newtype == null) {
922 // type never defined
923 // #TBD#: replace new ParseNode with original parsenode
925 if (!field.getPtr()) {
926 /* Pointer types don't have to be defined */
927 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
931 assert newtype != null;
932 field.setType(newtype);
937 Iterator labels = type.getLabels();
939 while (labels.hasNext()) {
940 LabelDescriptor label = (LabelDescriptor) labels.next();
941 TypeDescriptor labeltype = label.getType();
943 assert labeltype != null;
945 // check that the type is valid
946 if (labeltype instanceof MissingTypeDescriptor) {
947 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
948 if (newtype == null) {
949 // type never defined
950 // #TBD#: replace new ParseNode with original parsenode
951 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
954 assert newtype != null;
955 label.setType(newtype);
961 throw new IRException("shouldn't be any other typedescriptor classes");
969 types = stTypes.getDescriptors();
971 while (types.hasMoreElements()) {
972 TypeDescriptor t = (TypeDescriptor) types.nextElement();
974 if (t instanceof ReservedTypeDescriptor) {
975 // we don't need to check reserved types
976 } else if (t instanceof StructureTypeDescriptor) {
978 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
979 TypeDescriptor subtype = type.getSuperType();
980 Iterator fields = type.getFields();
982 while (fields.hasNext()) {
983 FieldDescriptor field = (FieldDescriptor) fields.next();
985 if (field instanceof ArrayDescriptor) {
986 ArrayDescriptor ad = (ArrayDescriptor) field;
987 Expr indexbound = ad.getIndexBound();
988 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
989 public IRErrorReporter getErrorReporter() { return er; }
990 public SymbolTable getSymbolTable() { return stGlobals; }
993 if (indextype == null) {
995 } else if (indextype != ReservedTypeDescriptor.INT) {
996 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
1002 Iterator labels = type.getLabels();
1004 while (labels.hasNext()) {
1005 LabelDescriptor label = (LabelDescriptor) labels.next();
1006 Expr index = label.getIndex();
1008 if (index != null) {
1009 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
1010 public IRErrorReporter getErrorReporter() { return er; }
1011 public SymbolTable getSymbolTable() { return stGlobals; }
1014 if (indextype != ReservedTypeDescriptor.INT) {
1015 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
1021 throw new IRException("shouldn't be any other typedescriptor classes");
1025 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
1026 // subtypes, of course, are not real subtypes, they are merely a way to validate a
1032 private boolean parse_global(ParseNode pn) {
1033 if (!precheck(pn, "global")) {
1037 String name = pn.getChild("name").getTerminal();
1038 assert name != null;
1040 String type = pn.getChild("type").getTerminal();
1041 assert type != null;
1042 TypeDescriptor td = lookupType(type);
1044 assert !(td instanceof ReservedTypeDescriptor);
1046 if (stGlobals.contains(name)) {
1047 /* redefinition of global */
1048 er.report(pn, "Redefinition of global '" + name + "'");
1052 stGlobals.add(new VarDescriptor(name, name, td,true));
1056 private boolean parse_structure(ParseNode pn) {
1057 if (!precheck(pn, "structure")) {
1062 String typename = pn.getChild("name").getTerminal();
1063 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1065 if (pn.getChild("subtype") != null) {
1066 // has a subtype, lets try to resolve it
1067 String subtype = pn.getChild("subtype").getTerminal();
1069 if (subtype.equals(typename)) {
1070 // Semantic Error: cyclic inheritance
1071 er.report(pn, "Cyclic inheritance prohibited");
1075 /* lookup the type to get the type descriptor */
1076 type.setSuperType(lookupType(subtype, CREATE_MISSING));
1077 } else if (pn.getChild("subclass") != null) {
1078 // has a subtype, lets try to resolve it
1079 String subclass = pn.getChild("subclass").getTerminal();
1081 if (subclass.equals(typename)) {
1082 // Semantic Error: cyclic inheritance
1083 er.report(pn, "Cyclic inheritance prohibited");
1087 /* lookup the type to get the type descriptor */
1088 type.setSuperType(lookupType(subclass, CREATE_MISSING));
1089 type.setSubClass(true);
1092 // set the current type so that the recursive parses on the labels
1093 // and fields can add themselves automatically to the current type
1094 dCurrentType = type;
1096 // parse the labels and fields
1097 if (!parse_labelsandfields(pn.getChild("lf"))) {
1101 if (stTypes.contains(typename)) {
1102 er.report(pn, "Redefinition of type '" + typename + "'");
1111 private boolean parse_labelsandfields(ParseNode pn) {
1112 if (!precheck(pn, "lf")) {
1118 // check the fields first (need the field names
1119 // to type check the labels)
1120 if (!parse_fields(pn.getChild("fields"))) {
1124 // check the labels now that all the fields are sorted
1125 if (!parse_labels(pn.getChild("labels"))) {
1132 private boolean parse_fields(ParseNode pn) {
1133 if (!precheck(pn, "fields")) {
1139 /* NOTE: because the order of the fields is important when defining a data structure,
1140 and because the order is defined by the order of the fields defined in the field
1141 vector, its important that the parser returns the fields in the correct order */
1143 ParseNodeVector fields = pn.getChildren();
1145 for (int i = 0; i < fields.size(); i++) {
1146 ParseNode field = fields.elementAt(i);
1151 if (field.getChild("reserved") != null) {
1153 // #TBD#: it will be necessary for reserved field descriptors to generate
1154 // a unique symbol for the type descriptor requires it for its hashtable
1155 fd = new ReservedFieldDescriptor();
1158 name = field.getChild("name").getTerminal();
1159 fd = new FieldDescriptor(name);
1163 String type = field.getChild("type").getTerminal();
1164 boolean ptr = field.getChild("*") != null;
1167 fd.setType(lookupType(type, CREATE_MISSING));
1169 if (field.getChild("index") != null) {
1170 // field is an array, so create an array descriptor to wrap the
1171 // field descriptor and then replace the top level field descriptor with
1172 // this array descriptor
1173 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1175 // #ATTN#: do we really want to return an exception here?
1176 throw new IRException("invalid index expression");
1178 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1182 // add the current field to the current type
1183 if (reserved == false) {
1184 // lets double check that we are redefining a field
1185 if (dCurrentType.getField(name) != null) {
1186 // Semantic Error: field redefinition
1187 er.report(pn, "Redefinition of field '" + name + "'");
1190 dCurrentType.addField(fd);
1193 dCurrentType.addField(fd);
1200 private boolean parse_labels(ParseNode pn) {
1201 if (!precheck(pn, "labels")) {
1207 /* NOTE: parse_labels should be called after the fields have been parsed because any
1208 labels not found in the field set of the current type will be flagged as errors */
1210 ParseNodeVector labels = pn.getChildren();
1212 for (int i = 0; i < labels.size(); i++) {
1213 ParseNode label = labels.elementAt(i);
1214 String name = label.getChild("name").getTerminal();
1215 LabelDescriptor ld = new LabelDescriptor(name);
1217 if (label.getChild("index") != null) {
1218 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1220 /* #ATTN#: do we really want to return an exception here? */
1221 throw new IRException("Invalid expression");
1226 String type = label.getChild("type").getTerminal();
1228 ld.setType(lookupType(type, CREATE_MISSING));
1230 String field = label.getChild("field").getTerminal();
1231 FieldDescriptor fd = dCurrentType.getField(field);
1234 /* Semantic Error: Undefined field in label */
1235 er.report(label, "Undefined field '" + field + "' in label");
1241 /* add label to current type */
1242 if (dCurrentType.getLabel(name) != null) {
1243 /* semantic error: label redefinition */
1244 er.report(pn, "Redefinition of label '" + name + "'");
1247 dCurrentType.addLabel(ld);
1254 private Expr parse_expr(ParseNode pn) {
1255 if (!precheck(pn, "expr")) {
1259 if (pn.getChild("var") != null) {
1260 // we've got a variable reference... we'll have to scope check it later
1261 // when we are completely done... there are also some issues of cyclic definitions
1262 return new VarExpr(pn.getChild("var").getTerminal());
1263 } else if (pn.getChild("literal") != null) {
1264 return parse_literal(pn.getChild("literal"));
1265 } else if (pn.getChild("operator") != null) {
1266 return parse_operator(pn.getChild("operator"));
1267 } else if (pn.getChild("relation") != null) {
1268 return parse_relation(pn.getChild("relation"));
1269 } else if (pn.getChild("sizeof") != null) {
1270 return parse_sizeof(pn.getChild("sizeof"));
1271 } else if (pn.getChild("simple_expr") != null) {
1272 return parse_simple_expr(pn.getChild("simple_expr"));
1273 } else if (pn.getChild("elementof") != null) {
1274 return parse_elementof(pn.getChild("elementof"));
1275 } else if (pn.getChild("tupleof") != null) {
1276 return parse_tupleof(pn.getChild("tupleof"));
1277 } else if (pn.getChild("isvalid") != null) {
1278 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1281 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1286 private Expr parse_elementof(ParseNode pn) {
1287 if (!precheck(pn, "elementof")) {
1292 String setname = pn.getChild("name").getTerminal();
1293 assert setname != null;
1294 SetDescriptor sd = lookupSet(setname);
1297 er.report(pn, "Undefined set '" + setname + "'");
1301 /* get left side expr */
1302 Expr expr = parse_expr(pn.getChild("expr"));
1308 return new ElementOfExpr(expr, sd);
1311 private Expr parse_tupleof(ParseNode pn) {
1312 if (!precheck(pn, "tupleof")) {
1317 String relname = pn.getChild("name").getTerminal();
1318 assert relname != null;
1319 RelationDescriptor rd = lookupRelation(relname);
1322 er.report(pn, "Undefined relation '" + relname + "'");
1326 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1327 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1329 if ((left == null) || (right == null)) {
1333 return new TupleOfExpr(left, right, rd);
1336 private Expr parse_simple_expr(ParseNode pn) {
1337 if (!precheck(pn, "simple_expr")) {
1341 // only locations so far
1342 return parse_location(pn.getChild("location"));
1345 private Expr parse_location(ParseNode pn) {
1346 if (!precheck(pn, "location")) {
1350 if (pn.getChild("var") != null) {
1351 // should be changed into a namespace check */
1352 return new VarExpr(pn.getChild("var").getTerminal());
1353 } else if (pn.getChild("cast") != null) {
1354 return parse_cast(pn.getChild("cast"));
1355 } else if (pn.getChild("dot") != null) {
1356 return parse_dot(pn.getChild("dot"));
1358 throw new IRException();
1362 private RelationExpr parse_relation(ParseNode pn) {
1363 if (!precheck(pn, "relation")) {
1367 String relname = pn.getChild("name").getTerminal();
1368 boolean inverse = pn.getChild("inv") != null;
1369 Expr expr = parse_expr(pn.getChild("expr"));
1375 RelationDescriptor relation = lookupRelation(relname);
1377 if (relation == null) {
1378 /* Semantic Error: relation not definied" */
1379 er.report(pn, "Undefined relation '" + relname + "'");
1383 /* add usage so correct sets are created */
1384 relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1386 return new RelationExpr(expr, relation, inverse);
1389 private SizeofExpr parse_sizeof(ParseNode pn) {
1390 if (!precheck(pn, "sizeof")) {
1395 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1397 if (setexpr == null) {
1401 return new SizeofExpr(setexpr);
1404 private CastExpr parse_cast(ParseNode pn) {
1405 if (!precheck(pn, "cast")) {
1410 String typename = pn.getChild("type").getTerminal();
1411 assert typename != null;
1412 TypeDescriptor type = lookupType(typename);
1415 /* semantic error: undefined type in cast */
1416 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1421 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1427 return new CastExpr(type, expr);
1430 private SetExpr parse_setexpr(ParseNode pn) {
1431 if (!precheck(pn, "setexpr")) {
1435 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1437 if (pn.getChild("set") != null) {
1438 String setname = pn.getChild("set").getTerminal();
1439 assert setname != null;
1440 SetDescriptor sd = lookupSet(setname);
1443 er.report(pn, "Unknown or undefined set '" + setname + "'");
1446 return new SetExpr(sd);
1448 } else if (pn.getChild("dot") != null) {
1449 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1450 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1451 relation.addUsage(RelationDescriptor.IMAGE);
1452 return new ImageSetExpr(vd, relation);
1453 } else if (pn.getChild("dotinv") != null) {
1454 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1455 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1456 relation.addUsage(RelationDescriptor.INVIMAGE);
1457 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1458 } else if (pn.getChild("dotset") != null) {
1459 ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotset").getChild("setexpr"));
1460 RelationDescriptor relation = lookupRelation(pn.getChild("dotset").getChild("relation").getTerminal());
1461 relation.addUsage(RelationDescriptor.IMAGE);
1462 return new ImageSetExpr(ise, relation);
1463 } else if (pn.getChild("dotinvset") != null) {
1464 ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotinvset").getChild("setexpr"));
1465 RelationDescriptor relation = lookupRelation(pn.getChild("dotinvset").getChild("relation").getTerminal());
1466 relation.addUsage(RelationDescriptor.INVIMAGE);
1467 return new ImageSetExpr(ImageSetExpr.INVERSE, ise, relation);
1469 throw new IRException();
1473 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1474 if (!precheck(pn, "quantifiervar")) {
1479 String varname = pn.getTerminal();
1480 assert varname != null;
1482 /* NOTE: quantifier var's are only found in the constraints and
1483 model definitions... therefore we can do a semantic check here
1484 to make sure that the variables exist in the symbol table */
1486 /* NOTE: its assumed that the symbol table stack is appropriately
1487 set up with the parent quantifier symbol table */
1488 assert !sts.empty();
1490 /* do semantic check and if valid, add it to symbol table
1491 and add it to the quantifier as well */
1492 if (sts.peek().contains(varname)) {
1493 VarDescriptor vdold=(VarDescriptor)sts.peek().get(varname);
1495 /* Dan was creating a new VarDescriptor...This seems
1496 like the wrong thing to do. We'll just lookup the
1498 --------------------------------------------------
1499 VarDescriptor vd=new VarDescriptor(varname);
1500 vd.setSet(vdold.getSet()); return vd;*/
1502 /* Semantic Error: undefined variable */
1503 er.report(pn, "Undefined variable '" + varname + "'");
1508 private LiteralExpr parse_literal(ParseNode pn) {
1509 if (!precheck(pn, "literal")) {
1513 if (pn.getChild("boolean") != null) {
1514 if (pn.getChild("boolean").getChild("true") != null) {
1515 return new BooleanLiteralExpr(true);
1517 return new BooleanLiteralExpr(false);
1519 } else if (pn.getChild("decimal") != null) {
1520 String integer = pn.getChild("decimal").getTerminal();
1522 /* Check for integer literal overflow */
1523 BigInteger intLitBI = new BigInteger(integer);
1524 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1525 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1528 if (intLitBI.compareTo(intMin) < 0) {
1529 value = Integer.MIN_VALUE;
1530 er.warn(pn, "Integer literal overflow");
1531 } else if (intLitBI.compareTo(intMax) > 0) {
1532 value = Integer.MAX_VALUE;
1533 er.warn(pn, "Integer literal overflow");
1535 /* no truncation needed */
1536 value = Integer.parseInt(integer);
1539 return new IntegerLiteralExpr(value);
1540 } else if (pn.getChild("token") != null) {
1541 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1542 } else if (pn.getChild("string") != null) {
1543 throw new IRException("string unsupported");
1544 } else if (pn.getChild("char") != null) {
1545 throw new IRException("char unsupported");
1547 throw new IRException("unknown literal expression type.");
1551 private OpExpr parse_operator(ParseNode pn) {
1552 if (!precheck(pn, "operator")) {
1556 String opname = pn.getChild("op").getTerminal();
1557 Opcode opcode = Opcode.decodeFromString(opname);
1559 if (opcode == null) {
1560 er.report(pn, "Unsupported operation: " + opname);
1564 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1567 if (pn.getChild("right") != null) {
1568 right = parse_expr(pn.getChild("right").getChild("expr"));
1575 if (right == null && opcode != Opcode.NOT) {
1576 er.report(pn, "Two arguments required.");
1580 return new OpExpr(opcode, left, right);
1583 private DotExpr parse_dot(ParseNode pn) {
1584 if (!precheck(pn, "dot")) {
1588 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1594 String field = pn.getChild("field").getTerminal();
1598 if (pn.getChild("index") != null) {
1599 index = parse_expr(pn.getChild("index").getChild("expr"));
1601 if (index == null) {
1606 return new DotExpr(left, field, index);