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?) */
396 private boolean parse_constraint(ParseNode pn) {
397 if (!precheck(pn, "constraint")) {
402 Constraint constraint = new Constraint();
405 boolean crash = pn.getChild("crash") != null;
406 constraint.setCrash(crash);
408 /* set up symbol table for constraint */
410 sts.push(constraint.getSymbolTable());
412 /* get quantifiers */
413 if (pn.getChild("quantifiers") != null) {
414 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
416 for (int i = 0; i < quantifiers.size(); i++) {
417 ParseNode qn = quantifiers.elementAt(i);
418 assert qn.getLabel().equals("quantifier");
419 Quantifier quantifier = parse_quantifier(qn);
420 if (quantifier == null) {
423 constraint.addQuantifier(quantifier);
429 LogicStatement logicexpr = parse_body(pn.getChild("body"));
431 if (logicexpr == null) {
434 constraint.setLogicStatement(logicexpr);
437 /* pop symbol table stack */
438 SymbolTable st = sts.pop();
440 /* make sure the stack we pop is our constraint s.t. */
441 assert st == constraint.getSymbolTable();
444 /* add to vConstraints */
445 vConstraints.addElement(constraint);
450 private Quantifier parse_quantifier(ParseNode pn) {
451 if (!precheck(pn, "quantifier")) {
455 if (pn.getChild("forall") != null) { /* forall element in Set */
456 SetQuantifier sq = new SetQuantifier();
459 VarDescriptor vd = reserveName(pn.getChild("var"));
468 SetDescriptor set = parse_set(pn.getChild("set"));
472 vd.setType(set.getType());
474 /* return to caller */
477 } else if (pn.getChild("relation") != null) { /* for < v1, v2 > in Relation */
478 RelationQuantifier rq = new RelationQuantifier();
481 VarDescriptor vd1 = reserveName(pn.getChild("left"));
482 VarDescriptor vd2 = reserveName(pn.getChild("right"));
484 if ((vd1 == null) || (vd2 == null)) {
488 rq.setTuple(vd1, vd2);
491 String relationname = pn.getChild("relation").getTerminal();
492 assert relationname != null;
493 RelationDescriptor rd = lookupRelation(relationname);
500 vd1.setType(rd.getDomain().getType());
501 vd2.setType(rd.getRange().getType());
503 } else if (pn.getChild("for") != null) { /* for j = x to y */
504 ForQuantifier fq = new ForQuantifier();
507 VarDescriptor vd = reserveName(pn.getChild("var"));
513 vd.setType(ReservedTypeDescriptor.INT);
516 /* grab lower/upper bounds */
517 Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
518 Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
520 if ((lower == null) || (upper == null)) {
524 fq.setBounds(lower, upper);
528 throw new IRException("not supported yet");
532 private LogicStatement parse_body(ParseNode pn) {
533 if (!precheck(pn, "body")) {
537 if (pn.getChild("and") != null) {
539 LogicStatement left, right;
540 left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
541 right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
543 if ((left == null) || (right == null)) {
547 // what do we want to call the and/or/not body classes?
548 return new LogicStatement(LogicStatement.AND, left, right);
549 } else if (pn.getChild("or") != null) {
551 LogicStatement left, right;
552 left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
553 right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
555 if ((left == null) || (right == null)) {
559 return new LogicStatement(LogicStatement.OR, left, right);
560 } else if (pn.getChild("not") != null) {
562 LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
568 return new LogicStatement(LogicStatement.NOT, left);
569 } else if (pn.getChild("predicate") != null) {
570 return parse_predicate(pn.getChild("predicate"));
572 throw new IRException();
576 private Predicate parse_predicate(ParseNode pn) {
577 if (!precheck(pn, "predicate")) {
581 if (pn.getChild("inclusion") != null) {
582 ParseNode in = pn.getChild("inclusion");
585 Expr expr = parse_expr(in.getChild("expr"));
592 SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
594 if (setexpr == null) {
598 return new InclusionPredicate(expr, setexpr);
599 } else if (pn.getChild("expr") != null) {
600 Expr expr = parse_expr(pn.getChild("expr"));
606 return new ExprPredicate(expr);
608 throw new IRException();
612 private SetDescriptor parse_set(ParseNode pn) {
613 if (!precheck(pn, "set")) {
617 if (pn.getChild("name") != null) {
618 String setname = pn.getChild("name").getTerminal();
619 assert setname != null;
621 if (!stSets.contains(setname)) {
622 /* Semantic Error: unknown set */
623 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
626 /* all good, get setdescriptor */
627 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
631 } else if (pn.getChild("listofliterals") != null) {
632 TokenSetDescriptor tokenset = new TokenSetDescriptor();
633 ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
634 assert token_literals.size() > 0;
636 for (int i = 0; i < token_literals.size(); i++) {
637 ParseNode literal = token_literals.elementAt(i);
638 assert literal.getLabel().equals("literal");
639 LiteralExpr litexpr = parse_literal(literal);
641 if (litexpr == null) {
645 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
646 tokenset.addLiteral(litexpr);
648 er.report(literal, "Elements of a user-defined set must be of type token or integer");
649 // return null; /* don't think we need to return null */
655 throw new IRException(pn.getTerminal());
659 private boolean parse_space(ParseNode pn) {
660 if (!precheck(pn, "space")) {
665 ParseNodeVector sets = pn.getChildren("setdefinition");
666 ParseNodeVector relations = pn.getChildren("relationdefinition");
668 assert pn.getChildren().size() == (sets.size() + relations.size());
671 for (int i = 0; i < sets.size(); i++) {
672 if (!parse_setdefinition(sets.elementAt(i))) {
677 /* parse relations */
678 for (int i = 0; i < relations.size(); i++) {
679 if (!parse_relationdefinition(relations.elementAt(i))) {
684 // ok, all the spaces have been parsed, now we should typecheck and check
687 // #TBD#: typecheck and check for cycles
689 /* replace missing with actual */
690 Iterator allsets = state.stSets.descriptors();
692 while (allsets.hasNext()) {
693 SetDescriptor sd = (SetDescriptor) allsets.next();
694 Vector subsets = sd.getSubsets();
696 for (int i = 0; i < subsets.size(); i++) {
697 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
699 if (subset instanceof MissingSetDescriptor) {
700 SetDescriptor newsubset = lookupSet(subset.getSymbol());
702 if (newsubset == null) {
703 er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
705 subsets.setElementAt(newsubset, i);
714 private boolean parse_setdefinition(ParseNode pn) {
715 if (!precheck(pn, "setdefinition")) {
722 String setname = pn.getChild("name").getTerminal();
723 assert (setname != null);
725 SetDescriptor sd = new SetDescriptor(setname);
728 String settype = pn.getChild("type").getTerminal();
729 TypeDescriptor type = lookupType(settype);
731 er.report(pn, "Undefined type '" + settype + "'");
737 /* is this a partition? */
738 boolean partition = pn.getChild("partition") != null;
739 sd.isPartition(partition);
741 /* if set has subsets, add them to set descriptor */
742 if (pn.getChild("setlist") != null) {
743 ParseNodeVector setlist = pn.getChild("setlist").getChildren();
745 for (int i = 0; i < setlist.size(); i++) {
746 String subsetname = setlist.elementAt(i).getLabel();
747 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
751 /* add set to symbol table */
752 if (stSets.contains(setname)) {
753 // Semantic Check: redefinition
754 er.report(pn, "Redefinition of set: " + setname);
763 private boolean parse_relationdefinition(ParseNode pn) {
764 if (!precheck(pn, "relationdefinition")) {
770 /* get relation name */
771 String relname = pn.getChild("name").getTerminal();
772 assert relname != null;
774 RelationDescriptor rd = new RelationDescriptor(relname);
776 /* check if static */
777 boolean bStatic = pn.getChild("static") != null;
778 rd.isStatic(bStatic);
781 String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
782 assert domainsetname != null;
785 String rangesetname = pn.getChild("range").getChild("type").getTerminal();
786 assert rangesetname != null;
788 /* get domain multiplicity */
790 if (pn.getChild("domain").getChild("domainmult") != null)
791 domainmult = pn.getChild("domain").getChild("domainmult").getChild("mult").getTerminal();
792 //assert domainmult != null;
794 /* get range multiplicity */
796 if (pn.getChild("range").getChild("domainrange") != null)
797 rangemult = pn.getChild("range").getChild("domainrange").getChild("mult").getTerminal();
798 //assert rangemult != null;
800 /* NOTE: it is assumed that the sets have been parsed already so that the
801 set namespace is fully populated. any missing setdescriptors for the set
802 symbol table will be assumed to be errors and reported. */
804 SetDescriptor domainset = lookupSet(domainsetname);
805 if (domainset == null) {
806 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
809 rd.setDomain(domainset);
812 SetDescriptor rangeset = lookupSet(rangesetname);
813 if (rangeset == null) {
814 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
817 rd.setRange(rangeset);
820 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
822 /* lets add the relation to the global symbol table */
823 if (!stRelations.contains(relname)) {
826 er.report(pn, "Redefinition of relation '" + relname + "'");
833 private boolean parse_structures(ParseNode pn) {
834 if (!precheck(pn, "structures")) {
839 ParseNodeVector structures = pn.getChildren("structure");
841 for (int i = 0; i < structures.size(); i++) {
842 if (!parse_structure(structures.elementAt(i))) {
847 ParseNodeVector globals = pn.getChildren("global");
849 for (int i = 0; i < globals.size(); i++) {
850 if (!parse_global(globals.elementAt(i))) {
855 // ok, all the structures have been parsed, now we gotta type check
857 Enumeration types = stTypes.getDescriptors();
858 while (types.hasMoreElements()) {
859 TypeDescriptor t = (TypeDescriptor) types.nextElement();
861 if (t instanceof ReservedTypeDescriptor) {
862 // we don't need to check reserved types
863 } else if (t instanceof StructureTypeDescriptor) {
865 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
866 TypeDescriptor subtype = type.getSuperType();
868 // check that the subtype is valid
869 if (subtype instanceof MissingTypeDescriptor) {
870 TypeDescriptor newtype = lookupType(subtype.getSymbol());
871 if (newtype == null) {
872 // subtype not defined anywheere
873 // #TBD#: somehow determine how we can get the original parsenode (global function?)
874 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
877 type.setSuperType(newtype);
881 Iterator fields = type.getFields();
883 while (fields.hasNext()) {
884 FieldDescriptor field = (FieldDescriptor) fields.next();
885 TypeDescriptor fieldtype = field.getType();
887 assert fieldtype != null;
889 // check that the type is valid
890 if (fieldtype instanceof MissingTypeDescriptor) {
891 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
892 if (newtype == null) {
893 // type never defined
894 // #TBD#: replace new ParseNode with original parsenode
895 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
898 assert newtype != null;
899 field.setType(newtype);
904 Iterator labels = type.getLabels();
906 while (labels.hasNext()) {
907 LabelDescriptor label = (LabelDescriptor) labels.next();
908 TypeDescriptor labeltype = label.getType();
910 assert labeltype != null;
912 // check that the type is valid
913 if (labeltype instanceof MissingTypeDescriptor) {
914 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
915 if (newtype == null) {
916 // type never defined
917 // #TBD#: replace new ParseNode with original parsenode
918 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
921 assert newtype != null;
922 label.setType(newtype);
928 throw new IRException("shouldn't be any other typedescriptor classes");
936 types = stTypes.getDescriptors();
938 while (types.hasMoreElements()) {
939 TypeDescriptor t = (TypeDescriptor) types.nextElement();
941 if (t instanceof ReservedTypeDescriptor) {
942 // we don't need to check reserved types
943 } else if (t instanceof StructureTypeDescriptor) {
945 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
946 TypeDescriptor subtype = type.getSuperType();
947 Iterator fields = type.getFields();
949 while (fields.hasNext()) {
950 FieldDescriptor field = (FieldDescriptor) fields.next();
952 if (field instanceof ArrayDescriptor) {
953 ArrayDescriptor ad = (ArrayDescriptor) field;
954 Expr indexbound = ad.getIndexBound();
955 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
956 public IRErrorReporter getErrorReporter() { return er; }
957 public SymbolTable getSymbolTable() { return stGlobals; }
960 if (indextype == null) {
962 } else if (indextype != ReservedTypeDescriptor.INT) {
963 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
969 Iterator labels = type.getLabels();
971 while (labels.hasNext()) {
972 LabelDescriptor label = (LabelDescriptor) labels.next();
973 Expr index = label.getIndex();
976 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
977 public IRErrorReporter getErrorReporter() { return er; }
978 public SymbolTable getSymbolTable() { return stGlobals; }
981 if (indextype != ReservedTypeDescriptor.INT) {
982 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
989 throw new IRException("shouldn't be any other typedescriptor classes");
994 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
995 // subtypes, of course, are not real subtypes, they are merely a way to validate a
1001 private boolean parse_global(ParseNode pn) {
1002 if (!precheck(pn, "global")) {
1006 String name = pn.getChild("name").getTerminal();
1007 assert name != null;
1009 String type = pn.getChild("type").getTerminal();
1010 assert type != null;
1011 TypeDescriptor td = lookupType(type);
1013 assert !(td instanceof ReservedTypeDescriptor);
1015 if (stGlobals.contains(name)) {
1016 /* redefinition of global */
1017 er.report(pn, "Redefinition of global '" + name + "'");
1021 stGlobals.add(new VarDescriptor(name, name, td,true));
1025 private boolean parse_structure(ParseNode pn) {
1026 if (!precheck(pn, "structure")) {
1031 String typename = pn.getChild("name").getTerminal();
1032 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1034 if (pn.getChild("subtype") != null) {
1035 // has a subtype, lets try to resolve it
1036 String subtype = pn.getChild("subtype").getTerminal();
1038 if (subtype.equals(typename)) {
1039 // Semantic Error: cyclic inheritance
1040 er.report(pn, "Cyclic inheritance prohibited");
1044 /* lookup the type to get the type descriptor */
1045 type.setSuperType(lookupType(subtype, CREATE_MISSING));
1048 // set the current type so that the recursive parses on the labels
1049 // and fields can add themselves automatically to the current type
1050 dCurrentType = type;
1052 // parse the labels and fields
1053 if (!parse_labelsandfields(pn.getChild("lf"))) {
1057 if (stTypes.contains(typename)) {
1058 er.report(pn, "Redefinition of type '" + typename + "'");
1067 private boolean parse_labelsandfields(ParseNode pn) {
1068 if (!precheck(pn, "lf")) {
1074 // check the fields first (need the field names
1075 // to type check the labels)
1076 if (!parse_fields(pn.getChild("fields"))) {
1080 // check the labels now that all the fields are sorted
1081 if (!parse_labels(pn.getChild("labels"))) {
1088 private boolean parse_fields(ParseNode pn) {
1089 if (!precheck(pn, "fields")) {
1095 /* NOTE: because the order of the fields is important when defining a data structure,
1096 and because the order is defined by the order of the fields defined in the field
1097 vector, its important that the parser returns the fields in the correct order */
1099 ParseNodeVector fields = pn.getChildren();
1101 for (int i = 0; i < fields.size(); i++) {
1102 ParseNode field = fields.elementAt(i);
1107 if (field.getChild("reserved") != null) {
1109 // #TBD#: it will be necessary for reserved field descriptors to generate
1110 // a unique symbol for the type descriptor requires it for its hashtable
1111 fd = new ReservedFieldDescriptor();
1114 name = field.getChild("name").getTerminal();
1115 fd = new FieldDescriptor(name);
1119 String type = field.getChild("type").getTerminal();
1120 boolean ptr = field.getChild("*") != null;
1123 fd.setType(lookupType(type, CREATE_MISSING));
1125 if (field.getChild("index") != null) {
1126 // field is an array, so create an array descriptor to wrap the
1127 // field descriptor and then replace the top level field descriptor with
1128 // this array descriptor
1129 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1131 // #ATTN#: do we really want to return an exception here?
1132 throw new IRException("invalid index expression");
1134 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1138 // add the current field to the current type
1139 if (reserved == false) {
1140 // lets double check that we are redefining a field
1141 if (dCurrentType.getField(name) != null) {
1142 // Semantic Error: field redefinition
1143 er.report(pn, "Redefinition of field '" + name + "'");
1146 dCurrentType.addField(fd);
1149 dCurrentType.addField(fd);
1156 private boolean parse_labels(ParseNode pn) {
1157 if (!precheck(pn, "labels")) {
1163 /* NOTE: parse_labels should be called after the fields have been parsed because any
1164 labels not found in the field set of the current type will be flagged as errors */
1166 ParseNodeVector labels = pn.getChildren();
1168 for (int i = 0; i < labels.size(); i++) {
1169 ParseNode label = labels.elementAt(i);
1170 String name = label.getChild("name").getTerminal();
1171 LabelDescriptor ld = new LabelDescriptor(name);
1173 if (label.getChild("index") != null) {
1174 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1176 /* #ATTN#: do we really want to return an exception here? */
1177 throw new IRException("Invalid expression");
1182 String type = label.getChild("type").getTerminal();
1184 ld.setType(lookupType(type, CREATE_MISSING));
1186 String field = label.getChild("field").getTerminal();
1187 FieldDescriptor fd = dCurrentType.getField(field);
1190 /* Semantic Error: Undefined field in label */
1191 er.report(label, "Undefined field '" + field + "' in label");
1197 /* add label to current type */
1198 if (dCurrentType.getLabel(name) != null) {
1199 /* semantic error: label redefinition */
1200 er.report(pn, "Redefinition of label '" + name + "'");
1203 dCurrentType.addLabel(ld);
1210 private Expr parse_expr(ParseNode pn) {
1211 if (!precheck(pn, "expr")) {
1215 if (pn.getChild("var") != null) {
1216 // we've got a variable reference... we'll have to scope check it later
1217 // when we are completely done... there are also some issues of cyclic definitions
1218 return new VarExpr(pn.getChild("var").getTerminal());
1219 } else if (pn.getChild("literal") != null) {
1220 return parse_literal(pn.getChild("literal"));
1221 } else if (pn.getChild("operator") != null) {
1222 return parse_operator(pn.getChild("operator"));
1223 } else if (pn.getChild("relation") != null) {
1224 return parse_relation(pn.getChild("relation"));
1225 } else if (pn.getChild("sizeof") != null) {
1226 return parse_sizeof(pn.getChild("sizeof"));
1227 } else if (pn.getChild("simple_expr") != null) {
1228 return parse_simple_expr(pn.getChild("simple_expr"));
1229 } else if (pn.getChild("elementof") != null) {
1230 return parse_elementof(pn.getChild("elementof"));
1231 } else if (pn.getChild("tupleof") != null) {
1232 return parse_tupleof(pn.getChild("tupleof"));
1233 } else if (pn.getChild("isvalid") != null) {
1234 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1237 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1242 private Expr parse_elementof(ParseNode pn) {
1243 if (!precheck(pn, "elementof")) {
1248 String setname = pn.getChild("name").getTerminal();
1249 assert setname != null;
1250 SetDescriptor sd = lookupSet(setname);
1253 er.report(pn, "Undefined set '" + setname + "'");
1257 /* get left side expr */
1258 Expr expr = parse_expr(pn.getChild("expr"));
1264 return new ElementOfExpr(expr, sd);
1267 private Expr parse_tupleof(ParseNode pn) {
1268 if (!precheck(pn, "tupleof")) {
1273 String relname = pn.getChild("name").getTerminal();
1274 assert relname != null;
1275 RelationDescriptor rd = lookupRelation(relname);
1278 er.report(pn, "Undefined relation '" + relname + "'");
1282 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1283 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1285 if ((left == null) || (right == null)) {
1289 return new TupleOfExpr(left, right, rd);
1292 private Expr parse_simple_expr(ParseNode pn) {
1293 if (!precheck(pn, "simple_expr")) {
1297 // only locations so far
1298 return parse_location(pn.getChild("location"));
1301 private Expr parse_location(ParseNode pn) {
1302 if (!precheck(pn, "location")) {
1306 if (pn.getChild("var") != null) {
1307 // should be changed into a namespace check */
1308 return new VarExpr(pn.getChild("var").getTerminal());
1309 } else if (pn.getChild("cast") != null) {
1310 return parse_cast(pn.getChild("cast"));
1311 } else if (pn.getChild("dot") != null) {
1312 return parse_dot(pn.getChild("dot"));
1314 throw new IRException();
1318 private RelationExpr parse_relation(ParseNode pn) {
1319 if (!precheck(pn, "relation")) {
1323 String relname = pn.getChild("name").getTerminal();
1324 boolean inverse = pn.getChild("inv") != null;
1325 Expr expr = parse_expr(pn.getChild("expr"));
1331 RelationDescriptor relation = lookupRelation(relname);
1333 if (relation == null) {
1334 /* Semantic Error: relation not definied" */
1335 er.report(pn, "Undefined relation '" + relname + "'");
1339 /* add usage so correct sets are created */
1340 relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1342 return new RelationExpr(expr, relation, inverse);
1345 private SizeofExpr parse_sizeof(ParseNode pn) {
1346 if (!precheck(pn, "sizeof")) {
1351 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1353 if (setexpr == null) {
1357 return new SizeofExpr(setexpr);
1360 private CastExpr parse_cast(ParseNode pn) {
1361 if (!precheck(pn, "cast")) {
1366 String typename = pn.getChild("type").getTerminal();
1367 assert typename != null;
1368 TypeDescriptor type = lookupType(typename);
1371 /* semantic error: undefined type in cast */
1372 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1377 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1383 return new CastExpr(type, expr);
1386 private SetExpr parse_setexpr(ParseNode pn) {
1387 if (!precheck(pn, "setexpr")) {
1391 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1393 if (pn.getChild("set") != null) {
1394 String setname = pn.getChild("set").getTerminal();
1395 assert setname != null;
1396 SetDescriptor sd = lookupSet(setname);
1399 er.report(pn, "Unknown or undefined set '" + setname + "'");
1402 return new SetExpr(sd);
1404 } else if (pn.getChild("dot") != null) {
1405 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1406 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1407 relation.addUsage(RelationDescriptor.IMAGE);
1408 return new ImageSetExpr(vd, relation);
1409 } else if (pn.getChild("dotinv") != null) {
1410 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1411 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1412 relation.addUsage(RelationDescriptor.INVIMAGE);
1413 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1415 throw new IRException();
1419 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1420 if (!precheck(pn, "quantifiervar")) {
1425 String varname = pn.getTerminal();
1426 assert varname != null;
1428 /* NOTE: quantifier var's are only found in the constraints and
1429 model definitions... therefore we can do a semantic check here
1430 to make sure that the variables exist in the symbol table */
1432 /* NOTE: its assumed that the symbol table stack is appropriately
1433 set up with the parent quantifier symbol table */
1434 assert !sts.empty();
1436 /* do semantic check and if valid, add it to symbol table
1437 and add it to the quantifier as well */
1438 if (sts.peek().contains(varname)) {
1439 return new VarDescriptor(varname);
1441 /* Semantic Error: undefined variable */
1442 er.report(pn, "Undefined variable '" + varname + "'");
1447 private LiteralExpr parse_literal(ParseNode pn) {
1448 if (!precheck(pn, "literal")) {
1452 if (pn.getChild("boolean") != null) {
1453 if (pn.getChild("boolean").getChild("true") != null) {
1454 return new BooleanLiteralExpr(true);
1456 return new BooleanLiteralExpr(false);
1458 } else if (pn.getChild("decimal") != null) {
1459 String integer = pn.getChild("decimal").getTerminal();
1461 /* Check for integer literal overflow */
1462 BigInteger intLitBI = new BigInteger(integer);
1463 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1464 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1467 if (intLitBI.compareTo(intMin) < 0) {
1468 value = Integer.MIN_VALUE;
1469 er.warn(pn, "Integer literal overflow");
1470 } else if (intLitBI.compareTo(intMax) > 0) {
1471 value = Integer.MAX_VALUE;
1472 er.warn(pn, "Integer literal overflow");
1474 /* no truncation needed */
1475 value = Integer.parseInt(integer);
1478 return new IntegerLiteralExpr(value);
1479 } else if (pn.getChild("token") != null) {
1480 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1481 } else if (pn.getChild("string") != null) {
1482 throw new IRException("string unsupported");
1483 } else if (pn.getChild("char") != null) {
1484 throw new IRException("char unsupported");
1486 throw new IRException("unknown literal expression type.");
1490 private OpExpr parse_operator(ParseNode pn) {
1491 if (!precheck(pn, "operator")) {
1495 String opname = pn.getChild("op").getTerminal();
1496 Opcode opcode = Opcode.decodeFromString(opname);
1498 if (opcode == null) {
1499 er.report(pn, "Unsupported operation: " + opname);
1503 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1506 if (pn.getChild("right") != null) {
1507 right = parse_expr(pn.getChild("right").getChild("expr"));
1514 if (right == null && opcode != Opcode.NOT) {
1515 er.report(pn, "Two arguments required.");
1519 return new OpExpr(opcode, left, right);
1522 private DotExpr parse_dot(ParseNode pn) {
1523 if (!precheck(pn, "dot")) {
1527 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1533 String field = pn.getChild("field").getTerminal();
1537 if (pn.getChild("index") != null) {
1538 index = parse_expr(pn.getChild("index").getChild("expr"));
1540 if (index == null) {
1545 return new DotExpr(left, field, index);