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("relatiion") != 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");
533 private LogicStatement parse_body(ParseNode pn) {
534 if (!precheck(pn, "body")) {
538 if (pn.getChild("and") != null) {
540 LogicStatement left, right;
541 left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
542 right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
544 if ((left == null) || (right == null)) {
548 // what do we want to call the and/or/not body classes?
549 return new LogicStatement(LogicStatement.AND, left, right);
550 } else if (pn.getChild("or") != null) {
552 LogicStatement left, right;
553 left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
554 right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
556 if ((left == null) || (right == null)) {
560 return new LogicStatement(LogicStatement.OR, left, right);
561 } else if (pn.getChild("not") != null) {
563 LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
569 return new LogicStatement(LogicStatement.NOT, left);
570 } else if (pn.getChild("predicate") != null) {
571 return parse_predicate(pn.getChild("predicate"));
573 throw new IRException();
577 private Predicate parse_predicate(ParseNode pn) {
578 if (!precheck(pn, "predicate")) {
582 if (pn.getChild("inclusion") != null) {
583 ParseNode in = pn.getChild("inclusion");
586 Expr expr = parse_expr(in.getChild("expr"));
593 SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
595 if (setexpr == null) {
599 return new InclusionPredicate(expr, setexpr);
600 } else if (pn.getChild("expr") != null) {
601 Expr expr = parse_expr(pn.getChild("expr"));
607 return new ExprPredicate(expr);
609 throw new IRException();
613 private SetDescriptor parse_set(ParseNode pn) {
614 if (!precheck(pn, "set")) {
618 if (pn.getChild("name") != null) {
619 String setname = pn.getChild("name").getTerminal();
620 assert setname != null;
622 if (!stSets.contains(setname)) {
623 /* Semantic Error: unknown set */
624 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
627 /* all good, get setdescriptor */
628 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
632 } else if (pn.getChild("listofliterals") != null) {
633 TokenSetDescriptor tokenset = new TokenSetDescriptor();
634 ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
635 assert token_literals.size() > 0;
637 for (int i = 0; i < token_literals.size(); i++) {
638 ParseNode literal = token_literals.elementAt(i);
639 assert literal.getLabel().equals("literal");
640 LiteralExpr litexpr = parse_literal(literal);
642 if (litexpr == null) {
646 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
647 tokenset.addLiteral(litexpr);
649 er.report(literal, "Elements of a user-defined set must be of type token or integer");
650 // return null; /* don't think we need to return null */
656 throw new IRException(pn.getTerminal());
660 private boolean parse_space(ParseNode pn) {
661 if (!precheck(pn, "space")) {
666 ParseNodeVector sets = pn.getChildren("setdefinition");
667 ParseNodeVector relations = pn.getChildren("relationdefinition");
669 assert pn.getChildren().size() == (sets.size() + relations.size());
672 for (int i = 0; i < sets.size(); i++) {
673 if (!parse_setdefinition(sets.elementAt(i))) {
678 /* parse relations */
679 for (int i = 0; i < relations.size(); i++) {
680 if (!parse_relationdefinition(relations.elementAt(i))) {
685 // ok, all the spaces have been parsed, now we should typecheck and check
688 // #TBD#: typecheck and check for cycles
690 /* replace missing with actual */
691 Iterator allsets = state.stSets.descriptors();
693 while (allsets.hasNext()) {
694 SetDescriptor sd = (SetDescriptor) allsets.next();
695 Vector subsets = sd.getSubsets();
697 for (int i = 0; i < subsets.size(); i++) {
698 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
700 if (subset instanceof MissingSetDescriptor) {
701 SetDescriptor newsubset = lookupSet(subset.getSymbol());
703 if (newsubset == null) {
704 er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
706 subsets.setElementAt(newsubset, i);
715 private boolean parse_setdefinition(ParseNode pn) {
716 if (!precheck(pn, "setdefinition")) {
723 String setname = pn.getChild("name").getTerminal();
724 assert (setname != null);
726 SetDescriptor sd = new SetDescriptor(setname);
729 String settype = pn.getChild("type").getTerminal();
730 TypeDescriptor type = lookupType(settype);
732 er.report(pn, "Undefined type '" + settype + "'");
738 /* is this a partition? */
739 boolean partition = pn.getChild("partition") != null;
740 sd.isPartition(partition);
742 /* if set has subsets, add them to set descriptor */
743 if (pn.getChild("setlist") != null) {
744 ParseNodeVector setlist = pn.getChild("setlist").getChildren();
746 for (int i = 0; i < setlist.size(); i++) {
747 String subsetname = setlist.elementAt(i).getLabel();
748 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
752 /* add set to symbol table */
753 if (stSets.contains(setname)) {
754 // Semantic Check: redefinition
755 er.report(pn, "Redefinition of set: " + setname);
764 private boolean parse_relationdefinition(ParseNode pn) {
765 if (!precheck(pn, "relationdefinition")) {
771 /* get relation name */
772 String relname = pn.getChild("name").getTerminal();
773 assert relname != null;
775 RelationDescriptor rd = new RelationDescriptor(relname);
777 /* check if static */
778 boolean bStatic = pn.getChild("static") != null;
779 rd.isStatic(bStatic);
782 String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
783 assert domainsetname != null;
786 String rangesetname = pn.getChild("range").getChild("type").getTerminal();
787 assert rangesetname != null;
789 /* get domain multiplicity */
790 String domainmult = pn.getChild("domain").getChild("mult").getTerminal();
791 assert domainmult != null;
793 /* get range multiplicity */
794 String rangemult = pn.getChild("range").getChild("mult").getTerminal();
795 assert rangemult != null;
797 /* NOTE: it is assumed that the sets have been parsed already so that the
798 set namespace is fully populated. any missing setdescriptors for the set
799 symbol table will be assumed to be errors and reported. */
801 SetDescriptor domainset = lookupSet(domainsetname);
802 if (domainset == null) {
803 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
806 rd.setDomain(domainset);
809 SetDescriptor rangeset = lookupSet(rangesetname);
810 if (rangeset == null) {
811 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
814 rd.setRange(rangeset);
817 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
819 /* lets add the relation to the global symbol table */
820 if (!stRelations.contains(relname)) {
823 er.report(pn, "Redefinition of relation '" + relname + "'");
830 private boolean parse_structures(ParseNode pn) {
831 if (!precheck(pn, "structures")) {
836 ParseNodeVector structures = pn.getChildren("structure");
838 for (int i = 0; i < structures.size(); i++) {
839 if (!parse_structure(structures.elementAt(i))) {
844 ParseNodeVector globals = pn.getChildren("global");
846 for (int i = 0; i < globals.size(); i++) {
847 if (!parse_global(globals.elementAt(i))) {
852 // ok, all the structures have been parsed, now we gotta type check
854 Enumeration types = stTypes.getDescriptors();
855 while (types.hasMoreElements()) {
856 TypeDescriptor t = (TypeDescriptor) types.nextElement();
858 if (t instanceof ReservedTypeDescriptor) {
859 // we don't need to check reserved types
860 } else if (t instanceof StructureTypeDescriptor) {
862 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
863 TypeDescriptor subtype = type.getSubType();
865 // check that the subtype is valid
866 if (subtype instanceof MissingTypeDescriptor) {
867 TypeDescriptor newtype = lookupType(subtype.getSymbol());
868 if (newtype == null) {
869 // subtype not defined anywheere
870 // #TBD#: somehow determine how we can get the original parsenode (global function?)
871 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
874 type.setSubType(newtype);
878 Iterator fields = type.getFields();
880 while (fields.hasNext()) {
881 FieldDescriptor field = (FieldDescriptor) fields.next();
882 TypeDescriptor fieldtype = field.getType();
884 assert fieldtype != null;
886 // check that the type is valid
887 if (fieldtype instanceof MissingTypeDescriptor) {
888 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
889 if (newtype == null) {
890 // type never defined
891 // #TBD#: replace new ParseNode with original parsenode
892 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
895 assert newtype != null;
896 field.setType(newtype);
901 Iterator labels = type.getLabels();
903 while (labels.hasNext()) {
904 LabelDescriptor label = (LabelDescriptor) labels.next();
905 TypeDescriptor labeltype = label.getType();
907 assert labeltype != null;
909 // check that the type is valid
910 if (labeltype instanceof MissingTypeDescriptor) {
911 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
912 if (newtype == null) {
913 // type never defined
914 // #TBD#: replace new ParseNode with original parsenode
915 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
918 assert newtype != null;
919 label.setType(newtype);
925 throw new IRException("shouldn't be any other typedescriptor classes");
933 types = stTypes.getDescriptors();
935 while (types.hasMoreElements()) {
936 TypeDescriptor t = (TypeDescriptor) types.nextElement();
938 if (t instanceof ReservedTypeDescriptor) {
939 // we don't need to check reserved types
940 } else if (t instanceof StructureTypeDescriptor) {
942 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
943 TypeDescriptor subtype = type.getSubType();
944 Iterator fields = type.getFields();
946 while (fields.hasNext()) {
947 FieldDescriptor field = (FieldDescriptor) fields.next();
949 if (field instanceof ArrayDescriptor) {
950 ArrayDescriptor ad = (ArrayDescriptor) field;
951 Expr indexbound = ad.getIndexBound();
952 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
953 public IRErrorReporter getErrorReporter() { return er; }
954 public SymbolTable getSymbolTable() { return stGlobals; }
957 if (indextype == null) {
959 } else if (indextype != ReservedTypeDescriptor.INT) {
960 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
966 Iterator labels = type.getLabels();
968 while (labels.hasNext()) {
969 LabelDescriptor label = (LabelDescriptor) labels.next();
970 Expr index = label.getIndex();
973 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
974 public IRErrorReporter getErrorReporter() { return er; }
975 public SymbolTable getSymbolTable() { return stGlobals; }
978 if (indextype != ReservedTypeDescriptor.INT) {
979 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
986 throw new IRException("shouldn't be any other typedescriptor classes");
991 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
992 // subtypes, of course, are not real subtypes, they are merely a way to validate a
998 private boolean parse_global(ParseNode pn) {
999 if (!precheck(pn, "global")) {
1003 String name = pn.getChild("name").getTerminal();
1004 assert name != null;
1006 String type = pn.getChild("type").getTerminal();
1007 assert type != null;
1008 TypeDescriptor td = lookupType(type);
1010 assert !(td instanceof ReservedTypeDescriptor);
1012 if (stGlobals.contains(name)) {
1013 /* redefinition of global */
1014 er.report(pn, "Redefinition of global '" + name + "'");
1018 stGlobals.add(new VarDescriptor(name, name, td));
1022 private boolean parse_structure(ParseNode pn) {
1023 if (!precheck(pn, "structure")) {
1028 String typename = pn.getChild("name").getTerminal();
1029 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1031 if (pn.getChild("subtype") != null) {
1032 // has a subtype, lets try to resolve it
1033 String subtype = pn.getChild("subtype").getTerminal();
1035 if (subtype.equals(typename)) {
1036 // Semantic Error: cyclic inheritance
1037 er.report(pn, "Cyclic inheritance prohibited");
1041 /* lookup the type to get the type descriptor */
1042 type.setSubType(lookupType(subtype, CREATE_MISSING));
1045 // set the current type so that the recursive parses on the labels
1046 // and fields can add themselves automatically to the current type
1047 dCurrentType = type;
1049 // parse the labels and fields
1050 if (!parse_labelsandfields(pn.getChild("lf"))) {
1054 if (stTypes.contains(typename)) {
1055 er.report(pn, "Redefinition of type '" + typename + "'");
1064 private boolean parse_labelsandfields(ParseNode pn) {
1065 if (!precheck(pn, "lf")) {
1071 // check the fields first (need the field names
1072 // to type check the labels)
1073 if (!parse_fields(pn.getChild("fields"))) {
1077 // check the labels now that all the fields are sorted
1078 if (!parse_labels(pn.getChild("labels"))) {
1085 private boolean parse_fields(ParseNode pn) {
1086 if (!precheck(pn, "fields")) {
1092 /* NOTE: because the order of the fields is important when defining a data structure,
1093 and because the order is defined by the order of the fields defined in the field
1094 vector, its important that the parser returns the fields in the correct order */
1096 ParseNodeVector fields = pn.getChildren();
1098 for (int i = 0; i < fields.size(); i++) {
1099 ParseNode field = fields.elementAt(i);
1104 if (field.getChild("reserved") != null) {
1106 // #TBD#: it will be necessary for reserved field descriptors to generate
1107 // a unique symbol for the type descriptor requires it for its hashtable
1108 fd = new ReservedFieldDescriptor();
1111 name = field.getChild("name").getTerminal();
1112 fd = new FieldDescriptor(name);
1116 String type = field.getChild("type").getTerminal();
1117 boolean ptr = field.getChild("*") != null;
1120 fd.setType(lookupType(type, CREATE_MISSING));
1122 if (field.getChild("index") != null) {
1123 // field is an array, so create an array descriptor to wrap the
1124 // field descriptor and then replace the top level field descriptor with
1125 // this array descriptor
1126 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1128 // #ATTN#: do we really want to return an exception here?
1129 throw new IRException("invalid index expression");
1131 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1135 // add the current field to the current type
1136 if (reserved == false) {
1137 // lets double check that we are redefining a field
1138 if (dCurrentType.getField(name) != null) {
1139 // Semantic Error: field redefinition
1140 er.report(pn, "Redefinition of field '" + name + "'");
1143 dCurrentType.addField(fd);
1146 dCurrentType.addField(fd);
1153 private boolean parse_labels(ParseNode pn) {
1154 if (!precheck(pn, "labels")) {
1160 /* NOTE: parse_labels should be called after the fields have been parsed because any
1161 labels not found in the field set of the current type will be flagged as errors */
1163 ParseNodeVector labels = pn.getChildren();
1165 for (int i = 0; i < labels.size(); i++) {
1166 ParseNode label = labels.elementAt(i);
1167 String name = label.getChild("name").getTerminal();
1168 LabelDescriptor ld = new LabelDescriptor(name);
1170 if (label.getChild("index") != null) {
1171 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1173 /* #ATTN#: do we really want to return an exception here? */
1174 throw new IRException("Invalid expression");
1179 String type = label.getChild("type").getTerminal();
1181 ld.setType(lookupType(type, CREATE_MISSING));
1183 String field = label.getChild("field").getTerminal();
1184 FieldDescriptor fd = dCurrentType.getField(field);
1187 /* Semantic Error: Undefined field in label */
1188 er.report(label, "Undefined field '" + field + "' in label");
1194 /* add label to current type */
1195 if (dCurrentType.getLabel(name) != null) {
1196 /* semantic error: label redefinition */
1197 er.report(pn, "Redefinition of label '" + name + "'");
1200 dCurrentType.addLabel(ld);
1207 private Expr parse_expr(ParseNode pn) {
1208 if (!precheck(pn, "expr")) {
1212 if (pn.getChild("var") != null) {
1213 // we've got a variable reference... we'll have to scope check it later
1214 // when we are completely done... there are also some issues of cyclic definitions
1215 return new VarExpr(pn.getChild("var").getTerminal());
1216 } else if (pn.getChild("literal") != null) {
1217 return parse_literal(pn.getChild("literal"));
1218 } else if (pn.getChild("operator") != null) {
1219 return parse_operator(pn.getChild("operator"));
1220 } else if (pn.getChild("relation") != null) {
1221 return parse_relation(pn.getChild("relation"));
1222 } else if (pn.getChild("sizeof") != null) {
1223 return parse_sizeof(pn.getChild("sizeof"));
1224 } else if (pn.getChild("simple_expr") != null) {
1225 return parse_simple_expr(pn.getChild("simple_expr"));
1226 } else if (pn.getChild("elementof") != null) {
1227 return parse_elementof(pn.getChild("elementof"));
1228 } else if (pn.getChild("tupleof") != null) {
1229 return parse_tupleof(pn.getChild("tupleof"));
1230 } else if (pn.getChild("isvalid") != null) {
1231 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1234 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1239 private Expr parse_elementof(ParseNode pn) {
1240 if (!precheck(pn, "elementof")) {
1245 String setname = pn.getChild("name").getTerminal();
1246 assert setname != null;
1247 SetDescriptor sd = lookupSet(setname);
1250 er.report(pn, "Undefined set '" + setname + "'");
1254 /* get left side expr */
1255 Expr expr = parse_expr(pn.getChild("expr"));
1261 return new ElementOfExpr(expr, sd);
1264 private Expr parse_tupleof(ParseNode pn) {
1265 if (!precheck(pn, "tupleof")) {
1270 String relname = pn.getChild("name").getTerminal();
1271 assert relname != null;
1272 RelationDescriptor rd = lookupRelation(relname);
1275 er.report(pn, "Undefined relation '" + relname + "'");
1279 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1280 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1282 if ((left == null) || (right == null)) {
1286 return new TupleOfExpr(left, right, rd);
1289 private Expr parse_simple_expr(ParseNode pn) {
1290 if (!precheck(pn, "simple_expr")) {
1294 // only locations so far
1295 return parse_location(pn.getChild("location"));
1298 private Expr parse_location(ParseNode pn) {
1299 if (!precheck(pn, "location")) {
1303 if (pn.getChild("var") != null) {
1304 // should be changed into a namespace check */
1305 return new VarExpr(pn.getChild("var").getTerminal());
1306 } else if (pn.getChild("cast") != null) {
1307 return parse_cast(pn.getChild("cast"));
1308 } else if (pn.getChild("dot") != null) {
1309 return parse_dot(pn.getChild("dot"));
1311 throw new IRException();
1315 private RelationExpr parse_relation(ParseNode pn) {
1316 if (!precheck(pn, "relation")) {
1320 String relname = pn.getChild("name").getTerminal();
1321 boolean inverse = pn.getChild("inv") != null;
1322 Expr expr = parse_expr(pn.getChild("expr"));
1328 RelationDescriptor relation = lookupRelation(relname);
1330 if (relation == null) {
1331 /* Semantic Error: relation not definied" */
1332 er.report(pn, "Undefined relation '" + relname + "'");
1336 /* add usage so correct sets are created */
1337 relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1339 return new RelationExpr(expr, relation, inverse);
1342 private SizeofExpr parse_sizeof(ParseNode pn) {
1343 if (!precheck(pn, "sizeof")) {
1348 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1350 if (setexpr == null) {
1354 return new SizeofExpr(setexpr);
1357 private CastExpr parse_cast(ParseNode pn) {
1358 if (!precheck(pn, "cast")) {
1363 String typename = pn.getChild("type").getTerminal();
1364 assert typename != null;
1365 TypeDescriptor type = lookupType(typename);
1368 /* semantic error: undefined type in cast */
1369 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1374 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1380 return new CastExpr(type, expr);
1383 private SetExpr parse_setexpr(ParseNode pn) {
1384 if (!precheck(pn, "setexpr")) {
1388 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1390 if (pn.getChild("set") != null) {
1391 String setname = pn.getChild("set").getTerminal();
1392 assert setname != null;
1393 SetDescriptor sd = lookupSet(setname);
1396 er.report(pn, "Unknown or undefined set '" + setname + "'");
1399 return new SetExpr(sd);
1401 } else if (pn.getChild("dot") != null) {
1402 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1403 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1404 relation.addUsage(RelationDescriptor.IMAGE);
1405 return new ImageSetExpr(vd, relation);
1406 } else if (pn.getChild("dotinv") != null) {
1407 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1408 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1409 relation.addUsage(RelationDescriptor.INVIMAGE);
1410 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1412 throw new IRException();
1416 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1417 if (!precheck(pn, "quantifiervar")) {
1422 String varname = pn.getTerminal();
1423 assert varname != null;
1425 /* NOTE: quantifier var's are only found in the constraints and
1426 model definitions... therefore we can do a semantic check here
1427 to make sure that the variables exist in the symbol table */
1429 /* NOTE: its assumed that the symbol table stack is appropriately
1430 set up with the parent quantifier symbol table */
1431 assert !sts.empty();
1433 /* do semantic check and if valid, add it to symbol table
1434 and add it to the quantifier as well */
1435 if (sts.peek().contains(varname)) {
1436 return new VarDescriptor(varname);
1438 /* Semantic Error: undefined variable */
1439 er.report(pn, "Undefined variable '" + varname + "'");
1444 private LiteralExpr parse_literal(ParseNode pn) {
1445 if (!precheck(pn, "literal")) {
1449 if (pn.getChild("boolean") != null) {
1450 if (pn.getChild("boolean").getChild("true") != null) {
1451 return new BooleanLiteralExpr(true);
1453 return new BooleanLiteralExpr(false);
1455 } else if (pn.getChild("decimal") != null) {
1456 String integer = pn.getChild("decimal").getTerminal();
1458 /* Check for integer literal overflow */
1459 BigInteger intLitBI = new BigInteger(integer);
1460 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1461 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1464 if (intLitBI.compareTo(intMin) < 0) {
1465 value = Integer.MIN_VALUE;
1466 er.warn(pn, "Integer literal overflow");
1467 } else if (intLitBI.compareTo(intMax) > 0) {
1468 value = Integer.MAX_VALUE;
1469 er.warn(pn, "Integer literal overflow");
1471 /* no truncation needed */
1472 value = Integer.parseInt(integer);
1475 return new IntegerLiteralExpr(value);
1476 } else if (pn.getChild("token") != null) {
1477 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1478 } else if (pn.getChild("string") != null) {
1479 throw new IRException("string unsupported");
1480 } else if (pn.getChild("char") != null) {
1481 throw new IRException("char unsupported");
1483 throw new IRException("unknown literal expression type.");
1487 private OpExpr parse_operator(ParseNode pn) {
1488 if (!precheck(pn, "operator")) {
1492 String opname = pn.getChild("op").getTerminal();
1493 Opcode opcode = Opcode.decodeFromString(opname);
1495 if (opcode == null) {
1496 er.report(pn, "Unsupported operation: " + opname);
1500 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1503 if (pn.getChild("right") != null) {
1504 right = parse_expr(pn.getChild("right").getChild("expr"));
1511 if (right == null && opcode != Opcode.NOT) {
1512 er.report(pn, "Two arguments required.");
1516 return new OpExpr(opcode, left, right);
1519 private DotExpr parse_dot(ParseNode pn) {
1520 if (!precheck(pn, "dot")) {
1524 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1530 String field = pn.getChild("field").getTerminal();
1534 if (pn.getChild("index") != null) {
1535 index = parse_expr(pn.getChild("index").getChild("expr"));
1537 if (index == null) {
1542 return new DotExpr(left, field, index);