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 */
789 String domainmult = pn.getChild("domain").getChild("mult").getTerminal();
790 assert domainmult != null;
792 /* get range multiplicity */
793 String rangemult = pn.getChild("range").getChild("mult").getTerminal();
794 assert rangemult != null;
796 /* NOTE: it is assumed that the sets have been parsed already so that the
797 set namespace is fully populated. any missing setdescriptors for the set
798 symbol table will be assumed to be errors and reported. */
800 SetDescriptor domainset = lookupSet(domainsetname);
801 if (domainset == null) {
802 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
805 rd.setDomain(domainset);
808 SetDescriptor rangeset = lookupSet(rangesetname);
809 if (rangeset == null) {
810 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
813 rd.setRange(rangeset);
816 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
818 /* lets add the relation to the global symbol table */
819 if (!stRelations.contains(relname)) {
822 er.report(pn, "Redefinition of relation '" + relname + "'");
829 private boolean parse_structures(ParseNode pn) {
830 if (!precheck(pn, "structures")) {
835 ParseNodeVector structures = pn.getChildren("structure");
837 for (int i = 0; i < structures.size(); i++) {
838 if (!parse_structure(structures.elementAt(i))) {
843 ParseNodeVector globals = pn.getChildren("global");
845 for (int i = 0; i < globals.size(); i++) {
846 if (!parse_global(globals.elementAt(i))) {
851 // ok, all the structures have been parsed, now we gotta type check
853 Enumeration types = stTypes.getDescriptors();
854 while (types.hasMoreElements()) {
855 TypeDescriptor t = (TypeDescriptor) types.nextElement();
857 if (t instanceof ReservedTypeDescriptor) {
858 // we don't need to check reserved types
859 } else if (t instanceof StructureTypeDescriptor) {
861 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
862 TypeDescriptor subtype = type.getSubType();
864 // check that the subtype is valid
865 if (subtype instanceof MissingTypeDescriptor) {
866 TypeDescriptor newtype = lookupType(subtype.getSymbol());
867 if (newtype == null) {
868 // subtype not defined anywheere
869 // #TBD#: somehow determine how we can get the original parsenode (global function?)
870 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
873 type.setSubType(newtype);
877 Iterator fields = type.getFields();
879 while (fields.hasNext()) {
880 FieldDescriptor field = (FieldDescriptor) fields.next();
881 TypeDescriptor fieldtype = field.getType();
883 assert fieldtype != null;
885 // check that the type is valid
886 if (fieldtype instanceof MissingTypeDescriptor) {
887 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
888 if (newtype == null) {
889 // type never defined
890 // #TBD#: replace new ParseNode with original parsenode
891 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
894 assert newtype != null;
895 field.setType(newtype);
900 Iterator labels = type.getLabels();
902 while (labels.hasNext()) {
903 LabelDescriptor label = (LabelDescriptor) labels.next();
904 TypeDescriptor labeltype = label.getType();
906 assert labeltype != null;
908 // check that the type is valid
909 if (labeltype instanceof MissingTypeDescriptor) {
910 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
911 if (newtype == null) {
912 // type never defined
913 // #TBD#: replace new ParseNode with original parsenode
914 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
917 assert newtype != null;
918 label.setType(newtype);
924 throw new IRException("shouldn't be any other typedescriptor classes");
932 types = stTypes.getDescriptors();
934 while (types.hasMoreElements()) {
935 TypeDescriptor t = (TypeDescriptor) types.nextElement();
937 if (t instanceof ReservedTypeDescriptor) {
938 // we don't need to check reserved types
939 } else if (t instanceof StructureTypeDescriptor) {
941 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
942 TypeDescriptor subtype = type.getSubType();
943 Iterator fields = type.getFields();
945 while (fields.hasNext()) {
946 FieldDescriptor field = (FieldDescriptor) fields.next();
948 if (field instanceof ArrayDescriptor) {
949 ArrayDescriptor ad = (ArrayDescriptor) field;
950 Expr indexbound = ad.getIndexBound();
951 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
952 public IRErrorReporter getErrorReporter() { return er; }
953 public SymbolTable getSymbolTable() { return stGlobals; }
956 if (indextype == null) {
958 } else if (indextype != ReservedTypeDescriptor.INT) {
959 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
965 Iterator labels = type.getLabels();
967 while (labels.hasNext()) {
968 LabelDescriptor label = (LabelDescriptor) labels.next();
969 Expr index = label.getIndex();
972 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
973 public IRErrorReporter getErrorReporter() { return er; }
974 public SymbolTable getSymbolTable() { return stGlobals; }
977 if (indextype != ReservedTypeDescriptor.INT) {
978 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
985 throw new IRException("shouldn't be any other typedescriptor classes");
990 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
991 // subtypes, of course, are not real subtypes, they are merely a way to validate a
997 private boolean parse_global(ParseNode pn) {
998 if (!precheck(pn, "global")) {
1002 String name = pn.getChild("name").getTerminal();
1003 assert name != null;
1005 String type = pn.getChild("type").getTerminal();
1006 assert type != null;
1007 TypeDescriptor td = lookupType(type);
1009 assert !(td instanceof ReservedTypeDescriptor);
1011 if (stGlobals.contains(name)) {
1012 /* redefinition of global */
1013 er.report(pn, "Redefinition of global '" + name + "'");
1017 stGlobals.add(new VarDescriptor(name, name, td));
1021 private boolean parse_structure(ParseNode pn) {
1022 if (!precheck(pn, "structure")) {
1027 String typename = pn.getChild("name").getTerminal();
1028 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1030 if (pn.getChild("subtype") != null) {
1031 // has a subtype, lets try to resolve it
1032 String subtype = pn.getChild("subtype").getTerminal();
1034 if (subtype.equals(typename)) {
1035 // Semantic Error: cyclic inheritance
1036 er.report(pn, "Cyclic inheritance prohibited");
1040 /* lookup the type to get the type descriptor */
1041 type.setSubType(lookupType(subtype, CREATE_MISSING));
1044 // set the current type so that the recursive parses on the labels
1045 // and fields can add themselves automatically to the current type
1046 dCurrentType = type;
1048 // parse the labels and fields
1049 if (!parse_labelsandfields(pn.getChild("lf"))) {
1053 if (stTypes.contains(typename)) {
1054 er.report(pn, "Redefinition of type '" + typename + "'");
1063 private boolean parse_labelsandfields(ParseNode pn) {
1064 if (!precheck(pn, "lf")) {
1070 // check the fields first (need the field names
1071 // to type check the labels)
1072 if (!parse_fields(pn.getChild("fields"))) {
1076 // check the labels now that all the fields are sorted
1077 if (!parse_labels(pn.getChild("labels"))) {
1084 private boolean parse_fields(ParseNode pn) {
1085 if (!precheck(pn, "fields")) {
1091 /* NOTE: because the order of the fields is important when defining a data structure,
1092 and because the order is defined by the order of the fields defined in the field
1093 vector, its important that the parser returns the fields in the correct order */
1095 ParseNodeVector fields = pn.getChildren();
1097 for (int i = 0; i < fields.size(); i++) {
1098 ParseNode field = fields.elementAt(i);
1103 if (field.getChild("reserved") != null) {
1105 // #TBD#: it will be necessary for reserved field descriptors to generate
1106 // a unique symbol for the type descriptor requires it for its hashtable
1107 fd = new ReservedFieldDescriptor();
1110 name = field.getChild("name").getTerminal();
1111 fd = new FieldDescriptor(name);
1115 String type = field.getChild("type").getTerminal();
1116 boolean ptr = field.getChild("*") != null;
1119 fd.setType(lookupType(type, CREATE_MISSING));
1121 if (field.getChild("index") != null) {
1122 // field is an array, so create an array descriptor to wrap the
1123 // field descriptor and then replace the top level field descriptor with
1124 // this array descriptor
1125 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1127 // #ATTN#: do we really want to return an exception here?
1128 throw new IRException("invalid index expression");
1130 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1134 // add the current field to the current type
1135 if (reserved == false) {
1136 // lets double check that we are redefining a field
1137 if (dCurrentType.getField(name) != null) {
1138 // Semantic Error: field redefinition
1139 er.report(pn, "Redefinition of field '" + name + "'");
1142 dCurrentType.addField(fd);
1145 dCurrentType.addField(fd);
1152 private boolean parse_labels(ParseNode pn) {
1153 if (!precheck(pn, "labels")) {
1159 /* NOTE: parse_labels should be called after the fields have been parsed because any
1160 labels not found in the field set of the current type will be flagged as errors */
1162 ParseNodeVector labels = pn.getChildren();
1164 for (int i = 0; i < labels.size(); i++) {
1165 ParseNode label = labels.elementAt(i);
1166 String name = label.getChild("name").getTerminal();
1167 LabelDescriptor ld = new LabelDescriptor(name);
1169 if (label.getChild("index") != null) {
1170 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1172 /* #ATTN#: do we really want to return an exception here? */
1173 throw new IRException("Invalid expression");
1178 String type = label.getChild("type").getTerminal();
1180 ld.setType(lookupType(type, CREATE_MISSING));
1182 String field = label.getChild("field").getTerminal();
1183 FieldDescriptor fd = dCurrentType.getField(field);
1186 /* Semantic Error: Undefined field in label */
1187 er.report(label, "Undefined field '" + field + "' in label");
1193 /* add label to current type */
1194 if (dCurrentType.getLabel(name) != null) {
1195 /* semantic error: label redefinition */
1196 er.report(pn, "Redefinition of label '" + name + "'");
1199 dCurrentType.addLabel(ld);
1206 private Expr parse_expr(ParseNode pn) {
1207 if (!precheck(pn, "expr")) {
1211 if (pn.getChild("var") != null) {
1212 // we've got a variable reference... we'll have to scope check it later
1213 // when we are completely done... there are also some issues of cyclic definitions
1214 return new VarExpr(pn.getChild("var").getTerminal());
1215 } else if (pn.getChild("literal") != null) {
1216 return parse_literal(pn.getChild("literal"));
1217 } else if (pn.getChild("operator") != null) {
1218 return parse_operator(pn.getChild("operator"));
1219 } else if (pn.getChild("relation") != null) {
1220 return parse_relation(pn.getChild("relation"));
1221 } else if (pn.getChild("sizeof") != null) {
1222 return parse_sizeof(pn.getChild("sizeof"));
1223 } else if (pn.getChild("simple_expr") != null) {
1224 return parse_simple_expr(pn.getChild("simple_expr"));
1225 } else if (pn.getChild("elementof") != null) {
1226 return parse_elementof(pn.getChild("elementof"));
1227 } else if (pn.getChild("tupleof") != null) {
1228 return parse_tupleof(pn.getChild("tupleof"));
1229 } else if (pn.getChild("isvalid") != null) {
1230 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1233 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1238 private Expr parse_elementof(ParseNode pn) {
1239 if (!precheck(pn, "elementof")) {
1244 String setname = pn.getChild("name").getTerminal();
1245 assert setname != null;
1246 SetDescriptor sd = lookupSet(setname);
1249 er.report(pn, "Undefined set '" + setname + "'");
1253 /* get left side expr */
1254 Expr expr = parse_expr(pn.getChild("expr"));
1260 return new ElementOfExpr(expr, sd);
1263 private Expr parse_tupleof(ParseNode pn) {
1264 if (!precheck(pn, "tupleof")) {
1269 String relname = pn.getChild("name").getTerminal();
1270 assert relname != null;
1271 RelationDescriptor rd = lookupRelation(relname);
1274 er.report(pn, "Undefined relation '" + relname + "'");
1278 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1279 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1281 if ((left == null) || (right == null)) {
1285 return new TupleOfExpr(left, right, rd);
1288 private Expr parse_simple_expr(ParseNode pn) {
1289 if (!precheck(pn, "simple_expr")) {
1293 // only locations so far
1294 return parse_location(pn.getChild("location"));
1297 private Expr parse_location(ParseNode pn) {
1298 if (!precheck(pn, "location")) {
1302 if (pn.getChild("var") != null) {
1303 // should be changed into a namespace check */
1304 return new VarExpr(pn.getChild("var").getTerminal());
1305 } else if (pn.getChild("cast") != null) {
1306 return parse_cast(pn.getChild("cast"));
1307 } else if (pn.getChild("dot") != null) {
1308 return parse_dot(pn.getChild("dot"));
1310 throw new IRException();
1314 private RelationExpr parse_relation(ParseNode pn) {
1315 if (!precheck(pn, "relation")) {
1319 String relname = pn.getChild("name").getTerminal();
1320 boolean inverse = pn.getChild("inv") != null;
1321 Expr expr = parse_expr(pn.getChild("expr"));
1327 RelationDescriptor relation = lookupRelation(relname);
1329 if (relation == null) {
1330 /* Semantic Error: relation not definied" */
1331 er.report(pn, "Undefined relation '" + relname + "'");
1335 /* add usage so correct sets are created */
1336 relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1338 return new RelationExpr(expr, relation, inverse);
1341 private SizeofExpr parse_sizeof(ParseNode pn) {
1342 if (!precheck(pn, "sizeof")) {
1347 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1349 if (setexpr == null) {
1353 return new SizeofExpr(setexpr);
1356 private CastExpr parse_cast(ParseNode pn) {
1357 if (!precheck(pn, "cast")) {
1362 String typename = pn.getChild("type").getTerminal();
1363 assert typename != null;
1364 TypeDescriptor type = lookupType(typename);
1367 /* semantic error: undefined type in cast */
1368 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1373 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1379 return new CastExpr(type, expr);
1382 private SetExpr parse_setexpr(ParseNode pn) {
1383 if (!precheck(pn, "setexpr")) {
1387 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1389 if (pn.getChild("set") != null) {
1390 String setname = pn.getChild("set").getTerminal();
1391 assert setname != null;
1392 SetDescriptor sd = lookupSet(setname);
1395 er.report(pn, "Unknown or undefined set '" + setname + "'");
1398 return new SetExpr(sd);
1400 } else if (pn.getChild("dot") != null) {
1401 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1402 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1403 relation.addUsage(RelationDescriptor.IMAGE);
1404 return new ImageSetExpr(vd, relation);
1405 } else if (pn.getChild("dotinv") != null) {
1406 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1407 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1408 relation.addUsage(RelationDescriptor.INVIMAGE);
1409 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1411 throw new IRException();
1415 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1416 if (!precheck(pn, "quantifiervar")) {
1421 String varname = pn.getTerminal();
1422 assert varname != null;
1424 /* NOTE: quantifier var's are only found in the constraints and
1425 model definitions... therefore we can do a semantic check here
1426 to make sure that the variables exist in the symbol table */
1428 /* NOTE: its assumed that the symbol table stack is appropriately
1429 set up with the parent quantifier symbol table */
1430 assert !sts.empty();
1432 /* do semantic check and if valid, add it to symbol table
1433 and add it to the quantifier as well */
1434 if (sts.peek().contains(varname)) {
1435 return new VarDescriptor(varname);
1437 /* Semantic Error: undefined variable */
1438 er.report(pn, "Undefined variable '" + varname + "'");
1443 private LiteralExpr parse_literal(ParseNode pn) {
1444 if (!precheck(pn, "literal")) {
1448 if (pn.getChild("boolean") != null) {
1449 if (pn.getChild("boolean").getChild("true") != null) {
1450 return new BooleanLiteralExpr(true);
1452 return new BooleanLiteralExpr(false);
1454 } else if (pn.getChild("decimal") != null) {
1455 String integer = pn.getChild("decimal").getTerminal();
1457 /* Check for integer literal overflow */
1458 BigInteger intLitBI = new BigInteger(integer);
1459 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1460 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1463 if (intLitBI.compareTo(intMin) < 0) {
1464 value = Integer.MIN_VALUE;
1465 er.warn(pn, "Integer literal overflow");
1466 } else if (intLitBI.compareTo(intMax) > 0) {
1467 value = Integer.MAX_VALUE;
1468 er.warn(pn, "Integer literal overflow");
1470 /* no truncation needed */
1471 value = Integer.parseInt(integer);
1474 return new IntegerLiteralExpr(value);
1475 } else if (pn.getChild("token") != null) {
1476 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1477 } else if (pn.getChild("string") != null) {
1478 throw new IRException("string unsupported");
1479 } else if (pn.getChild("char") != null) {
1480 throw new IRException("char unsupported");
1482 throw new IRException("unknown literal expression type.");
1486 private OpExpr parse_operator(ParseNode pn) {
1487 if (!precheck(pn, "operator")) {
1491 String opname = pn.getChild("op").getTerminal();
1492 Opcode opcode = Opcode.decodeFromString(opname);
1494 if (opcode == null) {
1495 er.report(pn, "Unsupported operation: " + opname);
1499 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1502 if (pn.getChild("right") != null) {
1503 right = parse_expr(pn.getChild("right").getChild("expr"));
1510 if (right == null && opcode != Opcode.NOT) {
1511 er.report(pn, "Two arguments required.");
1515 return new OpExpr(opcode, left, right);
1518 private DotExpr parse_dot(ParseNode pn) {
1519 if (!precheck(pn, "dot")) {
1523 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1529 String field = pn.getChild("field").getTerminal();
1533 if (pn.getChild("index") != null) {
1534 index = parse_expr(pn.getChild("index").getChild("expr"));
1536 if (index == null) {
1541 return new DotExpr(left, field, index);