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;
38 // Don't clear the state!! Do clear the IR-related state
39 this.state.stTypes = null;
42 throw new IRException("IRBuilder.build: Received null ErrorReporter");
47 if (state.ptStructures == null) {
48 throw new IRException("IRBuilder.build: Received null ParseNode");
51 state.vConstraints = new Vector();
52 vConstraints = state.vConstraints;
54 state.vRules = new Vector();
55 vRules = state.vRules;
57 state.stTypes = new SymbolTable();
58 stTypes = state.stTypes;
60 state.stSets = new SymbolTable();
61 stSets = state.stSets;
63 state.stRelations = new SymbolTable();
64 stRelations = state.stRelations;
66 state.stGlobals = new SymbolTable();
67 stGlobals = state.stGlobals;
69 sts = new SymbolTableStack();
71 // add int and bool to the types list
72 stTypes.add(ReservedTypeDescriptor.BIT);
73 stTypes.add(ReservedTypeDescriptor.BYTE);
74 stTypes.add(ReservedTypeDescriptor.SHORT);
75 stTypes.add(ReservedTypeDescriptor.INT);
77 stSets.add(new ReservedSetDescriptor("int", ReservedTypeDescriptor.INT));
78 stSets.add(new ReservedSetDescriptor("token", ReservedTypeDescriptor.INT));
82 er.setFilename(state.infile + ".struct");
83 if (!parse_structures(state.ptStructures)) {
87 er.setFilename(state.infile + ".space");
88 if (!parse_space(state.ptSpace)) {
92 er.setFilename(state.infile + ".constraints");
93 if (!parse_constraints(state.ptConstraints)) {
97 er.setFilename(state.infile + ".model");
98 if (!parse_rules(state.ptModel)) {
105 /********************** HELPER FUNCTIONS ************************/
108 * special case lookup that returns null if no such type exists
110 private TypeDescriptor lookupType(String typename) {
111 return lookupType(typename, false);
115 * does a look up in the types symbol table. if the type is
116 * not found than a missing type descriptor is returned
118 private TypeDescriptor lookupType(String typename, boolean createmissing) {
119 if (stTypes.get(typename) != null) {
120 // the type exists, so plug in the descriptor directly
121 return (TypeDescriptor) stTypes.get(typename);
122 } else if (createmissing) {
123 return new MissingTypeDescriptor(typename);
132 private VarDescriptor reserveName(ParseNode pn) {
134 String varname = pn.getTerminal();
135 assert varname != null;
137 /* do semantic check and if valid, add it to symbol table
138 and add it to the quantifier as well */
139 if (sts.peek().contains(varname)) {
140 /* Semantic Error: redefinition */
141 er.report(pn, "Redefinition of '" + varname + "'");
144 VarDescriptor vd = new VarDescriptor(varname);
151 * special case lookup that returns null if no such set exists
153 private SetDescriptor lookupSet(String setname) {
154 return lookupSet(setname, false);
158 * does a look up in the set's symbol table. if the set is
159 * not found than a missing set descriptor is returned
161 private SetDescriptor lookupSet(String setname, boolean createmissing) {
162 if (stSets.get(setname) != null) {
163 // the set exists, so plug in the descriptor directly
164 return (SetDescriptor) stSets.get(setname);
165 } else if (createmissing) {
166 return new MissingSetDescriptor(setname);
173 * does a look up in the set's symbol table. if the set is
174 * not found than a missing set descriptor is returned
176 private RelationDescriptor lookupRelation(String relname) {
177 if (stRelations.get(relname) != null) {
178 // the relation exists, so plug in the descriptor directly
179 return (RelationDescriptor) stRelations.get(relname);
186 private static int count = 0;
187 private boolean precheck(ParseNode pn, String label) {
189 er.report(pn, "IE: Expected '" + label + "', got null");
194 if (! pn.getLabel().equals(label)) {
195 er.report(pn, "IE: Expected '" + label + "', got '" + pn.getLabel() + "'");
200 if (state.verbose >= 2) {
201 System.err.println("visiting*" + (count++) + ": " + label);
207 /********************* PARSING FUNCTIONS ************************/
209 private boolean parse_rules(ParseNode pn) {
210 if (!precheck(pn, "rules")) {
215 ParseNodeVector rules = pn.getChildren();
217 for (int i = 0; i < rules.size(); i++) {
218 ParseNode rule = rules.elementAt(i);
219 if (!parse_rule(rule)) {
225 Iterator ruleiterator = state.vRules.iterator();
227 while (ruleiterator.hasNext()) {
228 Rule rule = (Rule) ruleiterator.next();
229 Expr guard = rule.getGuardExpr();
230 final SymbolTable rulest = rule.getSymbolTable();
231 SemanticAnalyzer sa = new SemanticAnalyzer() {
232 public IRErrorReporter getErrorReporter() { return er; }
233 public SymbolTable getSymbolTable() { return rulest; }
235 TypeDescriptor guardtype = guard.typecheck(sa);
237 if (guardtype == null) {
239 } else if (guardtype != ReservedTypeDescriptor.INT) {
240 er.report(null, "Type of guard must be 'int' not '" + guardtype.getSymbol() + "'");
244 if (!rule.getInclusion().typecheck(sa)) {
248 Iterator quantifiers = rule.quantifiers();
250 while (quantifiers.hasNext()) {
251 Quantifier q = (Quantifier) quantifiers.next();
253 if (q instanceof ForQuantifier && !((ForQuantifier)q).typecheck(sa)) {
259 /* do any post checks ?? */
264 private boolean parse_rule(ParseNode pn) {
265 if (!precheck(pn, "rule")) {
270 Rule rule = new Rule();
273 boolean isstatic = pn.getChild("static") != null;
274 boolean isdelay = pn.getChild("delay") != null;
275 rule.setStatic(isstatic);
276 rule.setDelay(isdelay);
278 /* set up symbol table for constraint */
281 sts.push(rule.getSymbolTable());
283 /* optional quantifiers */
284 if (pn.getChild("quantifiers") != null) {
285 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
287 for (int i = 0; i < quantifiers.size(); i++) {
288 ParseNode qn = quantifiers.elementAt(i);
289 Quantifier quantifier = parse_quantifier(qn);
291 if (quantifier == null) {
294 rule.addQuantifier(quantifier);
300 Expr guard = parse_expr(pn.getChild("expr"));
305 rule.setGuardExpr(guard);
308 /* inclusion constraint */
309 Inclusion inclusion = parse_inclusion(pn.getChild("inclusion"));
311 if (inclusion == null) {
314 rule.setInclusion(inclusion);
317 /* pop symbol table stack */
318 SymbolTable st = sts.pop();
319 sts.pop(); /* pop off globals */
321 /* make sure the stack we pop is our rule s.t. */
322 assert st == rule.getSymbolTable();
325 /* add rule to global set */
326 vRules.addElement(rule);
331 private Inclusion parse_inclusion(ParseNode pn) {
332 if (!precheck(pn, "inclusion")) {
336 if (pn.getChild("set") != null) {
337 ParseNode set = pn.getChild("set");
338 Expr expr = parse_expr(set.getChild("expr"));
344 String setname = set.getChild("name").getTerminal();
345 assert setname != null;
346 SetDescriptor sd = lookupSet(setname);
349 er.report(set.getChild("name"), "Undefined set '" + setname + "'");
353 return new SetInclusion(expr, sd);
354 } else if (pn.getChild("relation") != null) {
355 ParseNode relation = pn.getChild("relation");
356 Expr leftexpr = parse_expr(relation.getChild("left").getChild("expr"));
357 Expr rightexpr = parse_expr(relation.getChild("right").getChild("expr"));
359 if ((leftexpr == null) || (rightexpr == null)) {
363 String relname = relation.getChild("name").getTerminal();
364 assert relname != null;
365 RelationDescriptor rd = lookupRelation(relname);
368 er.report(relation.getChild("name"), "Undefined relation '" + relname + "'");
372 return new RelationInclusion(leftexpr, rightexpr, rd);
374 throw new IRException();
378 private boolean parse_constraints(ParseNode pn) {
379 if (!precheck(pn, "constraints")) {
384 ParseNodeVector constraints = pn.getChildren();
386 for (int i = 0; i < constraints.size(); i++) {
387 ParseNode constraint = constraints.elementAt(i);
388 assert constraint.getLabel().equals("constraint");
389 if (!parse_constraint(constraint)) {
394 /* do any post checks... (type constraints, etc?) */
399 private boolean parse_constraint(ParseNode pn) {
400 if (!precheck(pn, "constraint")) {
405 Constraint constraint = new Constraint();
408 boolean crash = pn.getChild("crash") != null;
409 constraint.setCrash(crash);
411 /* set up symbol table for constraint */
413 sts.push(constraint.getSymbolTable());
415 /* get quantifiers */
416 if (pn.getChild("quantifiers") != null) {
417 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
419 for (int i = 0; i < quantifiers.size(); i++) {
420 ParseNode qn = quantifiers.elementAt(i);
421 assert qn.getLabel().equals("quantifier");
422 Quantifier quantifier = parse_quantifier(qn);
423 if (quantifier == null) {
426 constraint.addQuantifier(quantifier);
432 LogicStatement logicexpr = parse_body(pn.getChild("body"));
434 if (logicexpr == null) {
437 constraint.setLogicStatement(logicexpr);
440 /* pop symbol table stack */
441 SymbolTable st = sts.pop();
443 /* make sure the stack we pop is our constraint s.t. */
444 assert st == constraint.getSymbolTable();
447 /* add to vConstraints */
448 vConstraints.addElement(constraint);
453 private Quantifier parse_quantifier(ParseNode pn) {
454 if (!precheck(pn, "quantifier")) {
458 if (pn.getChild("forall") != null) { /* forall element in Set */
459 SetQuantifier sq = new SetQuantifier();
462 VarDescriptor vd = reserveName(pn.getChild("var"));
471 SetDescriptor set = parse_set(pn.getChild("set"));
475 vd.setType(set.getType());
477 /* return to caller */
480 } else if (pn.getChild("relatiion") != null) { /* for < v1, v2 > in Relation */
481 RelationQuantifier rq = new RelationQuantifier();
484 VarDescriptor vd1 = reserveName(pn.getChild("left"));
485 VarDescriptor vd2 = reserveName(pn.getChild("right"));
487 if ((vd1 == null) || (vd2 == null)) {
491 rq.setTuple(vd1, vd2);
494 String relationname = pn.getChild("relation").getTerminal();
495 assert relationname != null;
496 RelationDescriptor rd = lookupRelation(relationname);
503 vd1.setType(rd.getDomain().getType());
504 vd2.setType(rd.getRange().getType());
506 } else if (pn.getChild("for") != null) { /* for j = x to y */
507 ForQuantifier fq = new ForQuantifier();
510 VarDescriptor vd = reserveName(pn.getChild("var"));
516 vd.setType(ReservedTypeDescriptor.INT);
519 /* grab lower/upper bounds */
520 Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
521 Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
523 if ((lower == null) || (upper == null)) {
527 fq.setBounds(lower, upper);
531 throw new IRException("not supported yet");
536 private LogicStatement parse_body(ParseNode pn) {
537 if (!precheck(pn, "body")) {
541 if (pn.getChild("and") != null) {
543 LogicStatement left, right;
544 left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
545 right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
547 if ((left == null) || (right == null)) {
551 // what do we want to call the and/or/not body classes?
552 return new LogicStatement(LogicStatement.AND, left, right);
553 } else if (pn.getChild("or") != null) {
555 LogicStatement left, right;
556 left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
557 right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
559 if ((left == null) || (right == null)) {
563 return new LogicStatement(LogicStatement.OR, left, right);
564 } else if (pn.getChild("not") != null) {
566 LogicStatement left = parse_body(pn.getChild("not").getChild("left").getChild("body"));
572 return new LogicStatement(LogicStatement.NOT, left);
573 } else if (pn.getChild("predicate") != null) {
574 return parse_predicate(pn.getChild("predicate"));
576 throw new IRException();
580 private Predicate parse_predicate(ParseNode pn) {
581 if (!precheck(pn, "predicate")) {
585 if (pn.getChild("comparison") != null) {
586 ParseNode cn = pn.getChild("comparison");
589 Expr left = parse_expr(cn.getChild("left").getChild("expr"));
590 Expr right = parse_expr(cn.getChild("right").getChild("expr"));
592 if ((left == null) || (right == null)) {
596 /* get comparison operator */
597 String comparison = cn.getChild("compare").getTerminal();
598 assert comparison != null;
600 return new ComparisonPredicate(comparison, left, right);
601 } else if (pn.getChild("inclusion") != null) {
602 ParseNode in = pn.getChild("inclusion");
604 /* get quantiifer var */
605 VarDescriptor vd = parse_quantifiervar(in.getChild("quantifiervar"));
612 SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
614 if (setexpr == null) {
618 return new InclusionPredicate(vd, setexpr);
620 throw new IRException();
624 private SetDescriptor parse_set(ParseNode pn) {
625 if (!precheck(pn, "set")) {
629 if (pn.getChild("name") != null) {
630 String setname = pn.getChild("name").getTerminal();
631 assert setname != null;
633 if (!stSets.contains(setname)) {
634 /* Semantic Error: unknown set */
635 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
638 /* all good, get setdescriptor */
639 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
643 } else if (pn.getChild("listofliterals") != null) {
644 TokenSetDescriptor tokenset = new TokenSetDescriptor();
645 ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
646 assert token_literals.size() > 0;
648 for (int i = 0; i < token_literals.size(); i++) {
649 ParseNode literal = token_literals.elementAt(i);
650 assert literal.getLabel().equals("literal");
651 LiteralExpr litexpr = parse_literal(literal);
653 if (litexpr == null) {
657 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
658 tokenset.addLiteral(litexpr);
660 er.report(literal, "Elements of a user-defined set must be of type token or integer");
661 // return null; /* don't think we need to return null */
667 throw new IRException(pn.getTerminal());
671 private boolean parse_space(ParseNode pn) {
672 if (!precheck(pn, "space")) {
677 ParseNodeVector sets = pn.getChildren("setdefinition");
678 ParseNodeVector relations = pn.getChildren("relationdefinition");
680 assert pn.getChildren().size() == (sets.size() + relations.size());
683 for (int i = 0; i < sets.size(); i++) {
684 if (!parse_setdefinition(sets.elementAt(i))) {
689 /* parse relations */
690 for (int i = 0; i < relations.size(); i++) {
691 if (!parse_relationdefinition(relations.elementAt(i))) {
696 // ok, all the spaces have been parsed, now we should typecheck and check
699 // #TBD#: typecheck and check for cycles
701 /* replace missing with actual */
702 Iterator allsets = state.stSets.descriptors();
704 while (allsets.hasNext()) {
705 SetDescriptor sd = (SetDescriptor) allsets.next();
706 Vector subsets = sd.getSubsets();
708 for (int i = 0; i < subsets.size(); i++) {
709 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
711 if (subset instanceof MissingSetDescriptor) {
712 SetDescriptor newsubset = lookupSet(subset.getSymbol());
714 if (newsubset == null) {
715 er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
717 subsets.setElementAt(newsubset, i);
726 private boolean parse_setdefinition(ParseNode pn) {
727 if (!precheck(pn, "setdefinition")) {
734 String setname = pn.getChild("name").getTerminal();
735 assert (setname != null);
737 SetDescriptor sd = new SetDescriptor(setname);
740 String settype = pn.getChild("type").getTerminal();
741 TypeDescriptor type = lookupType(settype);
743 er.report(pn, "Undefined type '" + settype + "'");
749 /* is this a partition? */
750 boolean partition = pn.getChild("partition") != null;
751 sd.isPartition(partition);
753 /* if set has subsets, add them to set descriptor */
754 if (pn.getChild("setlist") != null) {
755 ParseNodeVector setlist = pn.getChild("setlist").getChildren();
757 for (int i = 0; i < setlist.size(); i++) {
758 String subsetname = setlist.elementAt(i).getLabel();
759 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
763 /* add set to symbol table */
764 if (stSets.contains(setname)) {
765 // Semantic Check: redefinition
766 er.report(pn, "Redefinition of set: " + setname);
775 private boolean parse_relationdefinition(ParseNode pn) {
776 if (!precheck(pn, "relationdefinition")) {
782 /* get relation name */
783 String relname = pn.getChild("name").getTerminal();
784 assert relname != null;
786 RelationDescriptor rd = new RelationDescriptor(relname);
788 /* check if static */
789 boolean bStatic = pn.getChild("static") != null;
790 rd.isStatic(bStatic);
793 String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
794 assert domainsetname != null;
797 String rangesetname = pn.getChild("range").getChild("type").getTerminal();
798 assert rangesetname != null;
800 /* get domain multiplicity */
801 String domainmult = pn.getChild("domain").getChild("mult").getTerminal();
802 assert domainmult != null;
804 /* get range multiplicity */
805 String rangemult = pn.getChild("range").getChild("mult").getTerminal();
806 assert rangemult != null;
808 /* NOTE: it is assumed that the sets have been parsed already so that the
809 set namespace is fully populated. any missing setdescriptors for the set
810 symbol table will be assumed to be errors and reported. */
812 SetDescriptor domainset = lookupSet(domainsetname);
813 if (domainset == null) {
814 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
817 rd.setDomain(domainset);
820 SetDescriptor rangeset = lookupSet(rangesetname);
821 if (rangeset == null) {
822 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
825 rd.setRange(rangeset);
828 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
830 /* lets add the relation to the global symbol table */
831 if (!stRelations.contains(relname)) {
834 er.report(pn, "Redefinition of relation '" + relname + "'");
841 private boolean parse_structures(ParseNode pn) {
842 if (!precheck(pn, "structures")) {
847 ParseNodeVector structures = pn.getChildren("structure");
849 for (int i = 0; i < structures.size(); i++) {
850 if (!parse_structure(structures.elementAt(i))) {
855 ParseNodeVector globals = pn.getChildren("global");
857 for (int i = 0; i < globals.size(); i++) {
858 if (!parse_global(globals.elementAt(i))) {
863 // ok, all the structures have been parsed, now we gotta type check
865 Enumeration types = stTypes.getDescriptors();
866 while (types.hasMoreElements()) {
867 TypeDescriptor t = (TypeDescriptor) types.nextElement();
869 if (t instanceof ReservedTypeDescriptor) {
870 // we don't need to check reserved types
871 } else if (t instanceof StructureTypeDescriptor) {
873 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
874 TypeDescriptor subtype = type.getSubType();
876 // check that the subtype is valid
877 if (subtype instanceof MissingTypeDescriptor) {
878 TypeDescriptor newtype = lookupType(subtype.getSymbol());
879 if (newtype == null) {
880 // subtype not defined anywheere
881 // #TBD#: somehow determine how we can get the original parsenode (global function?)
882 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
885 type.setSubType(newtype);
889 Iterator fields = type.getFields();
891 while (fields.hasNext()) {
892 FieldDescriptor field = (FieldDescriptor) fields.next();
893 TypeDescriptor fieldtype = field.getType();
895 assert fieldtype != null;
897 // check that the type is valid
898 if (fieldtype instanceof MissingTypeDescriptor) {
899 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
900 if (newtype == null) {
901 // type never defined
902 // #TBD#: replace new ParseNode with original parsenode
903 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
906 assert newtype != null;
907 field.setType(newtype);
912 Iterator labels = type.getLabels();
914 while (labels.hasNext()) {
915 LabelDescriptor label = (LabelDescriptor) labels.next();
916 TypeDescriptor labeltype = label.getType();
918 assert labeltype != null;
920 // check that the type is valid
921 if (labeltype instanceof MissingTypeDescriptor) {
922 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
923 if (newtype == null) {
924 // type never defined
925 // #TBD#: replace new ParseNode with original parsenode
926 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
929 assert newtype != null;
930 label.setType(newtype);
936 throw new IRException("shouldn't be any other typedescriptor classes");
944 types = stTypes.getDescriptors();
946 while (types.hasMoreElements()) {
947 TypeDescriptor t = (TypeDescriptor) types.nextElement();
949 if (t instanceof ReservedTypeDescriptor) {
950 // we don't need to check reserved types
951 } else if (t instanceof StructureTypeDescriptor) {
953 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
954 TypeDescriptor subtype = type.getSubType();
955 Iterator fields = type.getFields();
957 while (fields.hasNext()) {
958 FieldDescriptor field = (FieldDescriptor) fields.next();
960 if (field instanceof ArrayDescriptor) {
961 ArrayDescriptor ad = (ArrayDescriptor) field;
962 Expr indexbound = ad.getIndexBound();
963 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
964 public IRErrorReporter getErrorReporter() { return er; }
965 public SymbolTable getSymbolTable() { return stGlobals; }
968 if (indextype == null) {
970 } else if (indextype != ReservedTypeDescriptor.INT) {
971 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
977 Iterator labels = type.getLabels();
979 while (labels.hasNext()) {
980 LabelDescriptor label = (LabelDescriptor) labels.next();
981 Expr index = label.getIndex();
984 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
985 public IRErrorReporter getErrorReporter() { return er; }
986 public SymbolTable getSymbolTable() { return stGlobals; }
989 if (indextype != ReservedTypeDescriptor.INT) {
990 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
997 throw new IRException("shouldn't be any other typedescriptor classes");
1002 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
1003 // subtypes, of course, are not real subtypes, they are merely a way to validate a
1009 private boolean parse_global(ParseNode pn) {
1010 if (!precheck(pn, "global")) {
1014 String name = pn.getChild("name").getTerminal();
1015 assert name != null;
1017 String type = pn.getChild("type").getTerminal();
1018 assert type != null;
1019 TypeDescriptor td = lookupType(type);
1021 assert !(td instanceof ReservedTypeDescriptor);
1023 if (stGlobals.contains(name)) {
1024 /* redefinition of global */
1025 er.report(pn, "Redefinition of global '" + name + "'");
1029 stGlobals.add(new VarDescriptor(name, name, td));
1033 private boolean parse_structure(ParseNode pn) {
1034 if (!precheck(pn, "structure")) {
1039 String typename = pn.getChild("name").getTerminal();
1040 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1042 if (pn.getChild("subtype") != null) {
1043 // has a subtype, lets try to resolve it
1044 String subtype = pn.getChild("subtype").getTerminal();
1046 if (subtype.equals(typename)) {
1047 // Semantic Error: cyclic inheritance
1048 er.report(pn, "Cyclic inheritance prohibited");
1052 /* lookup the type to get the type descriptor */
1053 type.setSubType(lookupType(subtype, CREATE_MISSING));
1056 // set the current type so that the recursive parses on the labels
1057 // and fields can add themselves automatically to the current type
1058 dCurrentType = type;
1060 // parse the labels and fields
1061 if (!parse_labelsandfields(pn.getChild("lf"))) {
1065 if (stTypes.contains(typename)) {
1066 er.report(pn, "Redefinition of type '" + typename + "'");
1075 private boolean parse_labelsandfields(ParseNode pn) {
1076 if (!precheck(pn, "lf")) {
1082 // check the fields first (need the field names
1083 // to type check the labels)
1084 if (!parse_fields(pn.getChild("fields"))) {
1088 // check the labels now that all the fields are sorted
1089 if (!parse_labels(pn.getChild("labels"))) {
1096 private boolean parse_fields(ParseNode pn) {
1097 if (!precheck(pn, "fields")) {
1103 /* NOTE: because the order of the fields is important when defining a data structure,
1104 and because the order is defined by the order of the fields defined in the field
1105 vector, its important that the parser returns the fields in the correct order */
1107 ParseNodeVector fields = pn.getChildren();
1109 for (int i = 0; i < fields.size(); i++) {
1110 ParseNode field = fields.elementAt(i);
1115 if (field.getChild("reserved") != null) {
1117 // #TBD#: it will be necessary for reserved field descriptors to generate
1118 // a unique symbol for the type descriptor requires it for its hashtable
1119 fd = new ReservedFieldDescriptor();
1122 name = field.getChild("name").getTerminal();
1123 fd = new FieldDescriptor(name);
1127 String type = field.getChild("type").getTerminal();
1128 boolean ptr = field.getChild("*") != null;
1131 fd.setType(lookupType(type, CREATE_MISSING));
1133 if (field.getChild("index") != null) {
1134 // field is an array, so create an array descriptor to wrap the
1135 // field descriptor and then replace the top level field descriptor with
1136 // this array descriptor
1137 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1139 // #ATTN#: do we really want to return an exception here?
1140 throw new IRException("invalid index expression");
1142 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1146 // add the current field to the current type
1147 if (reserved == false) {
1148 // lets double check that we are redefining a field
1149 if (dCurrentType.getField(name) != null) {
1150 // Semantic Error: field redefinition
1151 er.report(pn, "Redefinition of field '" + name + "'");
1154 dCurrentType.addField(fd);
1157 dCurrentType.addField(fd);
1164 private boolean parse_labels(ParseNode pn) {
1165 if (!precheck(pn, "labels")) {
1171 /* NOTE: parse_labels should be called after the fields have been parsed because any
1172 labels not found in the field set of the current type will be flagged as errors */
1174 ParseNodeVector labels = pn.getChildren();
1176 for (int i = 0; i < labels.size(); i++) {
1177 ParseNode label = labels.elementAt(i);
1178 String name = label.getChild("name").getTerminal();
1179 LabelDescriptor ld = new LabelDescriptor(name);
1181 if (label.getChild("index") != null) {
1182 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1184 /* #ATTN#: do we really want to return an exception here? */
1185 throw new IRException("Invalid expression");
1190 String type = label.getChild("type").getTerminal();
1192 ld.setType(lookupType(type, CREATE_MISSING));
1194 String field = label.getChild("field").getTerminal();
1195 FieldDescriptor fd = dCurrentType.getField(field);
1198 /* Semantic Error: Undefined field in label */
1199 er.report(label, "Undefined field '" + field + "' in label");
1205 /* add label to current type */
1206 if (dCurrentType.getLabel(name) != null) {
1207 /* semantic error: label redefinition */
1208 er.report(pn, "Redefinition of label '" + name + "'");
1211 dCurrentType.addLabel(ld);
1218 private Expr parse_expr(ParseNode pn) {
1219 if (!precheck(pn, "expr")) {
1223 if (pn.getChild("var") != null) {
1224 // we've got a variable reference... we'll have to scope check it later
1225 // when we are completely done... there are also some issues of cyclic definitions
1226 return new VarExpr(pn.getChild("var").getTerminal());
1227 } else if (pn.getChild("literal") != null) {
1228 return parse_literal(pn.getChild("literal"));
1229 } else if (pn.getChild("operator") != null) {
1230 return parse_operator(pn.getChild("operator"));
1231 } else if (pn.getChild("relation") != null) {
1232 return parse_relation(pn.getChild("relation"));
1233 } else if (pn.getChild("sizeof") != null) {
1234 return parse_sizeof(pn.getChild("sizeof"));
1235 } else if (pn.getChild("simple_expr") != null) {
1236 return parse_simple_expr(pn.getChild("simple_expr"));
1237 } else if (pn.getChild("elementof") != null) {
1238 return parse_elementof(pn.getChild("elementof"));
1239 } else if (pn.getChild("tupleof") != null) {
1240 return parse_tupleof(pn.getChild("tupleof"));
1241 } else if (pn.getChild("isvalid") != null) {
1242 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1245 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1250 private Expr parse_elementof(ParseNode pn) {
1251 if (!precheck(pn, "elementof")) {
1256 String setname = pn.getChild("name").getTerminal();
1257 assert setname != null;
1258 SetDescriptor sd = lookupSet(setname);
1261 er.report(pn, "Undefined set '" + setname + "'");
1265 /* get left side expr */
1266 Expr expr = parse_expr(pn.getChild("expr"));
1272 return new ElementOfExpr(expr, sd);
1275 private Expr parse_tupleof(ParseNode pn) {
1276 if (!precheck(pn, "tupleof")) {
1281 String relname = pn.getChild("name").getTerminal();
1282 assert relname != null;
1283 RelationDescriptor rd = lookupRelation(relname);
1286 er.report(pn, "Undefined relation '" + relname + "'");
1290 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1291 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1293 if ((left == null) || (right == null)) {
1297 return new TupleOfExpr(left, right, rd);
1300 private Expr parse_simple_expr(ParseNode pn) {
1301 if (!precheck(pn, "simple_expr")) {
1305 // only locations so far
1306 return parse_location(pn.getChild("location"));
1309 private Expr parse_location(ParseNode pn) {
1310 if (!precheck(pn, "location")) {
1314 if (pn.getChild("var") != null) {
1315 // should be changed into a namespace check */
1316 return new VarExpr(pn.getChild("var").getTerminal());
1317 } else if (pn.getChild("cast") != null) {
1318 return parse_cast(pn.getChild("cast"));
1319 } else if (pn.getChild("dot") != null) {
1320 return parse_dot(pn.getChild("dot"));
1322 throw new IRException();
1326 private RelationExpr parse_relation(ParseNode pn) {
1327 if (!precheck(pn, "relation")) {
1331 RelationExpr re = new RelationExpr();
1333 /* get quantitifer var */
1334 VarDescriptor vd = parse_quantifiervar(pn.getChild("quantifiervar"));
1343 /* grab list of relations */
1344 ParseNodeVector relations = pn.getChild("relations").getChildren();
1345 assert relations.size() >= 1;
1347 // #TBD#: verify that the relations are in the correct order and that the
1348 // first relation is getting the correct "inv" assigned from "expr"
1350 /* lets verify that these relations are defined */
1351 for (int i = 0; i < relations.size(); i++) {
1352 ParseNode rn = relations.elementAt(i);
1353 String relname = rn.getLabel();
1354 boolean inverse = rn.getChild("inv") != null;
1356 RelationDescriptor relation = lookupRelation(relname);
1358 if (relation == null) {
1359 /* Semantic Error: relation not definied" */
1360 er.report(rn, "Undefined relation '" + relname + "'");
1364 re.setRelation(relation, inverse);
1366 /* if we are not at end of list then create new relation and
1367 replace it to chain the relations */
1368 if (i + 1 < relations.size()) {
1369 re = new RelationExpr(re); // should create relation with domain as older 're'
1376 private SizeofExpr parse_sizeof(ParseNode pn) {
1377 if (!precheck(pn, "sizeof")) {
1382 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1384 if (setexpr == null) {
1388 return new SizeofExpr(setexpr);
1391 private CastExpr parse_cast(ParseNode pn) {
1392 if (!precheck(pn, "cast")) {
1397 String typename = pn.getChild("type").getTerminal();
1398 assert typename != null;
1399 TypeDescriptor type = lookupType(typename);
1402 /* semantic error: undefined type in cast */
1403 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1408 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1414 return new CastExpr(type, expr);
1417 private SetExpr parse_setexpr(ParseNode pn) {
1418 if (!precheck(pn, "setexpr")) {
1422 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1424 if (pn.getChild("set") != null) {
1425 String setname = pn.getChild("set").getTerminal();
1426 assert setname != null;
1427 SetDescriptor sd = lookupSet(setname);
1430 er.report(pn, "Unknown or undefined set '" + setname + "'");
1433 return new SetExpr(sd);
1435 } else if (pn.getChild("dot") != null) {
1436 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1437 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1438 return new ImageSetExpr(vd, relation);
1439 } else if (pn.getChild("dotinv") != null) {
1440 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1441 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1442 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1444 throw new IRException();
1448 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1449 if (!precheck(pn, "quantifiervar")) {
1454 String varname = pn.getTerminal();
1455 assert varname != null;
1457 /* NOTE: quantifier var's are only found in the constraints and
1458 model definitions... therefore we can do a semantic check here
1459 to make sure that the variables exist in the symbol table */
1461 /* NOTE: its assumed that the symbol table stack is appropriately
1462 set up with the parent quantifier symbol table */
1463 assert !sts.empty();
1465 /* do semantic check and if valid, add it to symbol table
1466 and add it to the quantifier as well */
1467 if (sts.peek().contains(varname)) {
1468 return new VarDescriptor(varname);
1470 /* Semantic Error: undefined variable */
1471 er.report(pn, "Undefined variable '" + varname + "'");
1476 private LiteralExpr parse_literal(ParseNode pn) {
1477 if (!precheck(pn, "literal")) {
1481 if (pn.getChild("boolean") != null) {
1482 if (pn.getChild("boolean").getChild("true") != null) {
1483 return new BooleanLiteralExpr(true);
1485 return new BooleanLiteralExpr(false);
1487 } else if (pn.getChild("decimal") != null) {
1488 String integer = pn.getChild("decimal").getTerminal();
1490 /* Check for integer literal overflow */
1491 BigInteger intLitBI = new BigInteger(integer);
1492 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1493 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1496 if (intLitBI.compareTo(intMin) < 0) {
1497 value = Integer.MIN_VALUE;
1498 er.warn(pn, "Integer literal overflow");
1499 } else if (intLitBI.compareTo(intMax) > 0) {
1500 value = Integer.MAX_VALUE;
1501 er.warn(pn, "Integer literal overflow");
1503 /* no truncation needed */
1504 value = Integer.parseInt(integer);
1507 return new IntegerLiteralExpr(value);
1508 } else if (pn.getChild("token") != null) {
1509 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1510 } else if (pn.getChild("string") != null) {
1511 throw new IRException("string unsupported");
1512 } else if (pn.getChild("char") != null) {
1513 throw new IRException("char unsupported");
1515 throw new IRException("unknown literal expression type.");
1519 private OpExpr parse_operator(ParseNode pn) {
1520 if (!precheck(pn, "operator")) {
1524 String opname = pn.getChild("op").getTerminal();
1528 if (opname.equals("add")) {
1529 opcode = Opcode.ADD;
1530 } else if (opname.equals("sub")) {
1531 opcode = Opcode.SUB;
1532 } else if (opname.equals("mult")) {
1533 opcode = Opcode.MULT;
1534 } else if (opname.equals("div")) {
1535 opcode = Opcode.DIV;
1536 } else if (opname.equals("and")) {
1537 opcode = Opcode.AND;
1538 } else if (opname.equals("or")) {
1540 } else if (opname.equals("not")) {
1541 opcode = Opcode.NOT;
1542 } else if (opname.equals("gt")) {
1544 } else if (opname.equals("ge")) {
1546 } else if (opname.equals("lt")) {
1548 } else if (opname.equals("le")) {
1550 } else if (opname.equals("eq")) {
1552 } else if (opname.equals("ne")) {
1555 er.report(pn, "Unsupported operation: " + opname);
1559 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1562 if (pn.getChild("right") != null) {
1563 right = parse_expr(pn.getChild("right").getChild("expr"));
1570 if (right == null && opcode != Opcode.NOT) {
1571 er.report(pn, "Two arguments required.");
1575 return new OpExpr(opcode, left, right);
1578 private DotExpr parse_dot(ParseNode pn) {
1579 if (!precheck(pn, "dot")) {
1583 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1589 String field = pn.getChild("field").getTerminal();
1593 if (pn.getChild("index") != null) {
1594 index = parse_expr(pn.getChild("index").getChild("expr"));
1596 if (index == null) {
1601 return new DotExpr(left, field, index);