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("left").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");
585 /* get quantiifer var */
586 VarDescriptor vd = parse_quantifiervar(in.getChild("quantifiervar"));
593 SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
595 if (setexpr == null) {
599 return new InclusionPredicate(vd, setexpr);
600 } else if (pn.getChild("sizeof") != null) {
601 ParseNode sizeof = pn.getChild("sizeof");
604 SetExpr setexpr = parse_setexpr(sizeof.getChild("setexpr"));
606 if (setexpr == null) {
610 /* get comparison operator */
611 String compareop = sizeof.getChild("compare").getTerminal();
612 Opcode opcode = Opcode.decodeFromString(compareop);
614 if (opcode == null) {
615 er.report(pn, "Unsupported operation '" + compareop + "'");
617 } else if (opcode != Opcode.EQ &&
618 opcode != Opcode.GE &&
619 opcode != Opcode.LE) {
620 er.report(pn, "Invalid operation '" + compareop + "': Must be one of '=', '>=', '<='");
625 String decimal = sizeof.getChild("decimal").getTerminal();
626 IntegerLiteralExpr cardinality = new IntegerLiteralExpr(Integer.parseInt(decimal));
628 return new SizeofPredicate(setexpr, opcode, cardinality);
629 } else if (pn.getChild("comparison") != null) {
630 ParseNode cn = pn.getChild("comparison");
632 /* get quantifier variable */
633 String varname = cn.getChild("quantifier").getTerminal();
634 String relation = cn.getChild("relation").getTerminal();
636 if (!sts.peek().contains(varname)) {
637 er.report(pn, "Undefined quantifier '" + varname + "'");
641 VarDescriptor vd = (VarDescriptor) sts.peek().get(varname);
643 if (!stRelations.contains(relation)) {
644 er.report(pn, "Undefined relation '" + varname + "'");
648 RelationDescriptor rd = (RelationDescriptor) stRelations.get(relation);
651 Expr expr = parse_expr(cn.getChild("expr"));
657 /* get comparison operator */
658 String compareop = cn.getChild("compare").getTerminal();
659 Opcode opcode = Opcode.decodeFromString(compareop);
661 if (opcode == null) {
662 er.report(pn, "Unsupported operation '" + compareop + "'");
664 } else if (opcode != Opcode.EQ &&
665 opcode != Opcode.GE &&
666 opcode != Opcode.LE) {
667 er.report(pn, "Invalid operation '" + compareop + "': Must be one of '=', '>=', '<='");
671 rd.addUsage(RelationDescriptor.IMAGE);
673 return new ComparisonPredicate(vd, rd, opcode, expr);
675 throw new IRException();
679 private SetDescriptor parse_set(ParseNode pn) {
680 if (!precheck(pn, "set")) {
684 if (pn.getChild("name") != null) {
685 String setname = pn.getChild("name").getTerminal();
686 assert setname != null;
688 if (!stSets.contains(setname)) {
689 /* Semantic Error: unknown set */
690 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
693 /* all good, get setdescriptor */
694 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
698 } else if (pn.getChild("listofliterals") != null) {
699 TokenSetDescriptor tokenset = new TokenSetDescriptor();
700 ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
701 assert token_literals.size() > 0;
703 for (int i = 0; i < token_literals.size(); i++) {
704 ParseNode literal = token_literals.elementAt(i);
705 assert literal.getLabel().equals("literal");
706 LiteralExpr litexpr = parse_literal(literal);
708 if (litexpr == null) {
712 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
713 tokenset.addLiteral(litexpr);
715 er.report(literal, "Elements of a user-defined set must be of type token or integer");
716 // return null; /* don't think we need to return null */
722 throw new IRException(pn.getTerminal());
726 private boolean parse_space(ParseNode pn) {
727 if (!precheck(pn, "space")) {
732 ParseNodeVector sets = pn.getChildren("setdefinition");
733 ParseNodeVector relations = pn.getChildren("relationdefinition");
735 assert pn.getChildren().size() == (sets.size() + relations.size());
738 for (int i = 0; i < sets.size(); i++) {
739 if (!parse_setdefinition(sets.elementAt(i))) {
744 /* parse relations */
745 for (int i = 0; i < relations.size(); i++) {
746 if (!parse_relationdefinition(relations.elementAt(i))) {
751 // ok, all the spaces have been parsed, now we should typecheck and check
754 // #TBD#: typecheck and check for cycles
756 /* replace missing with actual */
757 Iterator allsets = state.stSets.descriptors();
759 while (allsets.hasNext()) {
760 SetDescriptor sd = (SetDescriptor) allsets.next();
761 Vector subsets = sd.getSubsets();
763 for (int i = 0; i < subsets.size(); i++) {
764 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
766 if (subset instanceof MissingSetDescriptor) {
767 SetDescriptor newsubset = lookupSet(subset.getSymbol());
769 if (newsubset == null) {
770 er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
772 subsets.setElementAt(newsubset, i);
781 private boolean parse_setdefinition(ParseNode pn) {
782 if (!precheck(pn, "setdefinition")) {
789 String setname = pn.getChild("name").getTerminal();
790 assert (setname != null);
792 SetDescriptor sd = new SetDescriptor(setname);
795 String settype = pn.getChild("type").getTerminal();
796 TypeDescriptor type = lookupType(settype);
798 er.report(pn, "Undefined type '" + settype + "'");
804 /* is this a partition? */
805 boolean partition = pn.getChild("partition") != null;
806 sd.isPartition(partition);
808 /* if set has subsets, add them to set descriptor */
809 if (pn.getChild("setlist") != null) {
810 ParseNodeVector setlist = pn.getChild("setlist").getChildren();
812 for (int i = 0; i < setlist.size(); i++) {
813 String subsetname = setlist.elementAt(i).getLabel();
814 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
818 /* add set to symbol table */
819 if (stSets.contains(setname)) {
820 // Semantic Check: redefinition
821 er.report(pn, "Redefinition of set: " + setname);
830 private boolean parse_relationdefinition(ParseNode pn) {
831 if (!precheck(pn, "relationdefinition")) {
837 /* get relation name */
838 String relname = pn.getChild("name").getTerminal();
839 assert relname != null;
841 RelationDescriptor rd = new RelationDescriptor(relname);
843 /* check if static */
844 boolean bStatic = pn.getChild("static") != null;
845 rd.isStatic(bStatic);
848 String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
849 assert domainsetname != null;
852 String rangesetname = pn.getChild("range").getChild("type").getTerminal();
853 assert rangesetname != null;
855 /* get domain multiplicity */
856 String domainmult = pn.getChild("domain").getChild("mult").getTerminal();
857 assert domainmult != null;
859 /* get range multiplicity */
860 String rangemult = pn.getChild("range").getChild("mult").getTerminal();
861 assert rangemult != null;
863 /* NOTE: it is assumed that the sets have been parsed already so that the
864 set namespace is fully populated. any missing setdescriptors for the set
865 symbol table will be assumed to be errors and reported. */
867 SetDescriptor domainset = lookupSet(domainsetname);
868 if (domainset == null) {
869 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
872 rd.setDomain(domainset);
875 SetDescriptor rangeset = lookupSet(rangesetname);
876 if (rangeset == null) {
877 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
880 rd.setRange(rangeset);
883 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
885 /* lets add the relation to the global symbol table */
886 if (!stRelations.contains(relname)) {
889 er.report(pn, "Redefinition of relation '" + relname + "'");
896 private boolean parse_structures(ParseNode pn) {
897 if (!precheck(pn, "structures")) {
902 ParseNodeVector structures = pn.getChildren("structure");
904 for (int i = 0; i < structures.size(); i++) {
905 if (!parse_structure(structures.elementAt(i))) {
910 ParseNodeVector globals = pn.getChildren("global");
912 for (int i = 0; i < globals.size(); i++) {
913 if (!parse_global(globals.elementAt(i))) {
918 // ok, all the structures have been parsed, now we gotta type check
920 Enumeration types = stTypes.getDescriptors();
921 while (types.hasMoreElements()) {
922 TypeDescriptor t = (TypeDescriptor) types.nextElement();
924 if (t instanceof ReservedTypeDescriptor) {
925 // we don't need to check reserved types
926 } else if (t instanceof StructureTypeDescriptor) {
928 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
929 TypeDescriptor subtype = type.getSubType();
931 // check that the subtype is valid
932 if (subtype instanceof MissingTypeDescriptor) {
933 TypeDescriptor newtype = lookupType(subtype.getSymbol());
934 if (newtype == null) {
935 // subtype not defined anywheere
936 // #TBD#: somehow determine how we can get the original parsenode (global function?)
937 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
940 type.setSubType(newtype);
944 Iterator fields = type.getFields();
946 while (fields.hasNext()) {
947 FieldDescriptor field = (FieldDescriptor) fields.next();
948 TypeDescriptor fieldtype = field.getType();
950 assert fieldtype != null;
952 // check that the type is valid
953 if (fieldtype instanceof MissingTypeDescriptor) {
954 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
955 if (newtype == null) {
956 // type never defined
957 // #TBD#: replace new ParseNode with original parsenode
958 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
961 assert newtype != null;
962 field.setType(newtype);
967 Iterator labels = type.getLabels();
969 while (labels.hasNext()) {
970 LabelDescriptor label = (LabelDescriptor) labels.next();
971 TypeDescriptor labeltype = label.getType();
973 assert labeltype != null;
975 // check that the type is valid
976 if (labeltype instanceof MissingTypeDescriptor) {
977 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
978 if (newtype == null) {
979 // type never defined
980 // #TBD#: replace new ParseNode with original parsenode
981 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
984 assert newtype != null;
985 label.setType(newtype);
991 throw new IRException("shouldn't be any other typedescriptor classes");
999 types = stTypes.getDescriptors();
1001 while (types.hasMoreElements()) {
1002 TypeDescriptor t = (TypeDescriptor) types.nextElement();
1004 if (t instanceof ReservedTypeDescriptor) {
1005 // we don't need to check reserved types
1006 } else if (t instanceof StructureTypeDescriptor) {
1008 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
1009 TypeDescriptor subtype = type.getSubType();
1010 Iterator fields = type.getFields();
1012 while (fields.hasNext()) {
1013 FieldDescriptor field = (FieldDescriptor) fields.next();
1015 if (field instanceof ArrayDescriptor) {
1016 ArrayDescriptor ad = (ArrayDescriptor) field;
1017 Expr indexbound = ad.getIndexBound();
1018 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
1019 public IRErrorReporter getErrorReporter() { return er; }
1020 public SymbolTable getSymbolTable() { return stGlobals; }
1023 if (indextype == null) {
1025 } else if (indextype != ReservedTypeDescriptor.INT) {
1026 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
1032 Iterator labels = type.getLabels();
1034 while (labels.hasNext()) {
1035 LabelDescriptor label = (LabelDescriptor) labels.next();
1036 Expr index = label.getIndex();
1038 if (index != null) {
1039 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
1040 public IRErrorReporter getErrorReporter() { return er; }
1041 public SymbolTable getSymbolTable() { return stGlobals; }
1044 if (indextype != ReservedTypeDescriptor.INT) {
1045 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
1052 throw new IRException("shouldn't be any other typedescriptor classes");
1057 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
1058 // subtypes, of course, are not real subtypes, they are merely a way to validate a
1064 private boolean parse_global(ParseNode pn) {
1065 if (!precheck(pn, "global")) {
1069 String name = pn.getChild("name").getTerminal();
1070 assert name != null;
1072 String type = pn.getChild("type").getTerminal();
1073 assert type != null;
1074 TypeDescriptor td = lookupType(type);
1076 assert !(td instanceof ReservedTypeDescriptor);
1078 if (stGlobals.contains(name)) {
1079 /* redefinition of global */
1080 er.report(pn, "Redefinition of global '" + name + "'");
1084 stGlobals.add(new VarDescriptor(name, name, td));
1088 private boolean parse_structure(ParseNode pn) {
1089 if (!precheck(pn, "structure")) {
1094 String typename = pn.getChild("name").getTerminal();
1095 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1097 if (pn.getChild("subtype") != null) {
1098 // has a subtype, lets try to resolve it
1099 String subtype = pn.getChild("subtype").getTerminal();
1101 if (subtype.equals(typename)) {
1102 // Semantic Error: cyclic inheritance
1103 er.report(pn, "Cyclic inheritance prohibited");
1107 /* lookup the type to get the type descriptor */
1108 type.setSubType(lookupType(subtype, CREATE_MISSING));
1111 // set the current type so that the recursive parses on the labels
1112 // and fields can add themselves automatically to the current type
1113 dCurrentType = type;
1115 // parse the labels and fields
1116 if (!parse_labelsandfields(pn.getChild("lf"))) {
1120 if (stTypes.contains(typename)) {
1121 er.report(pn, "Redefinition of type '" + typename + "'");
1130 private boolean parse_labelsandfields(ParseNode pn) {
1131 if (!precheck(pn, "lf")) {
1137 // check the fields first (need the field names
1138 // to type check the labels)
1139 if (!parse_fields(pn.getChild("fields"))) {
1143 // check the labels now that all the fields are sorted
1144 if (!parse_labels(pn.getChild("labels"))) {
1151 private boolean parse_fields(ParseNode pn) {
1152 if (!precheck(pn, "fields")) {
1158 /* NOTE: because the order of the fields is important when defining a data structure,
1159 and because the order is defined by the order of the fields defined in the field
1160 vector, its important that the parser returns the fields in the correct order */
1162 ParseNodeVector fields = pn.getChildren();
1164 for (int i = 0; i < fields.size(); i++) {
1165 ParseNode field = fields.elementAt(i);
1170 if (field.getChild("reserved") != null) {
1172 // #TBD#: it will be necessary for reserved field descriptors to generate
1173 // a unique symbol for the type descriptor requires it for its hashtable
1174 fd = new ReservedFieldDescriptor();
1177 name = field.getChild("name").getTerminal();
1178 fd = new FieldDescriptor(name);
1182 String type = field.getChild("type").getTerminal();
1183 boolean ptr = field.getChild("*") != null;
1186 fd.setType(lookupType(type, CREATE_MISSING));
1188 if (field.getChild("index") != null) {
1189 // field is an array, so create an array descriptor to wrap the
1190 // field descriptor and then replace the top level field descriptor with
1191 // this array descriptor
1192 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1194 // #ATTN#: do we really want to return an exception here?
1195 throw new IRException("invalid index expression");
1197 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1201 // add the current field to the current type
1202 if (reserved == false) {
1203 // lets double check that we are redefining a field
1204 if (dCurrentType.getField(name) != null) {
1205 // Semantic Error: field redefinition
1206 er.report(pn, "Redefinition of field '" + name + "'");
1209 dCurrentType.addField(fd);
1212 dCurrentType.addField(fd);
1219 private boolean parse_labels(ParseNode pn) {
1220 if (!precheck(pn, "labels")) {
1226 /* NOTE: parse_labels should be called after the fields have been parsed because any
1227 labels not found in the field set of the current type will be flagged as errors */
1229 ParseNodeVector labels = pn.getChildren();
1231 for (int i = 0; i < labels.size(); i++) {
1232 ParseNode label = labels.elementAt(i);
1233 String name = label.getChild("name").getTerminal();
1234 LabelDescriptor ld = new LabelDescriptor(name);
1236 if (label.getChild("index") != null) {
1237 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1239 /* #ATTN#: do we really want to return an exception here? */
1240 throw new IRException("Invalid expression");
1245 String type = label.getChild("type").getTerminal();
1247 ld.setType(lookupType(type, CREATE_MISSING));
1249 String field = label.getChild("field").getTerminal();
1250 FieldDescriptor fd = dCurrentType.getField(field);
1253 /* Semantic Error: Undefined field in label */
1254 er.report(label, "Undefined field '" + field + "' in label");
1260 /* add label to current type */
1261 if (dCurrentType.getLabel(name) != null) {
1262 /* semantic error: label redefinition */
1263 er.report(pn, "Redefinition of label '" + name + "'");
1266 dCurrentType.addLabel(ld);
1273 private Expr parse_expr(ParseNode pn) {
1274 if (!precheck(pn, "expr")) {
1278 if (pn.getChild("var") != null) {
1279 // we've got a variable reference... we'll have to scope check it later
1280 // when we are completely done... there are also some issues of cyclic definitions
1281 return new VarExpr(pn.getChild("var").getTerminal());
1282 } else if (pn.getChild("literal") != null) {
1283 return parse_literal(pn.getChild("literal"));
1284 } else if (pn.getChild("operator") != null) {
1285 return parse_operator(pn.getChild("operator"));
1286 } else if (pn.getChild("relation") != null) {
1287 return parse_relation(pn.getChild("relation"));
1288 } else if (pn.getChild("sizeof") != null) {
1289 return parse_sizeof(pn.getChild("sizeof"));
1290 } else if (pn.getChild("simple_expr") != null) {
1291 return parse_simple_expr(pn.getChild("simple_expr"));
1292 } else if (pn.getChild("elementof") != null) {
1293 return parse_elementof(pn.getChild("elementof"));
1294 } else if (pn.getChild("tupleof") != null) {
1295 return parse_tupleof(pn.getChild("tupleof"));
1296 } else if (pn.getChild("isvalid") != null) {
1297 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1300 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1305 private Expr parse_elementof(ParseNode pn) {
1306 if (!precheck(pn, "elementof")) {
1311 String setname = pn.getChild("name").getTerminal();
1312 assert setname != null;
1313 SetDescriptor sd = lookupSet(setname);
1316 er.report(pn, "Undefined set '" + setname + "'");
1320 /* get left side expr */
1321 Expr expr = parse_expr(pn.getChild("expr"));
1327 return new ElementOfExpr(expr, sd);
1330 private Expr parse_tupleof(ParseNode pn) {
1331 if (!precheck(pn, "tupleof")) {
1336 String relname = pn.getChild("name").getTerminal();
1337 assert relname != null;
1338 RelationDescriptor rd = lookupRelation(relname);
1341 er.report(pn, "Undefined relation '" + relname + "'");
1345 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1346 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1348 if ((left == null) || (right == null)) {
1352 return new TupleOfExpr(left, right, rd);
1355 private Expr parse_simple_expr(ParseNode pn) {
1356 if (!precheck(pn, "simple_expr")) {
1360 // only locations so far
1361 return parse_location(pn.getChild("location"));
1364 private Expr parse_location(ParseNode pn) {
1365 if (!precheck(pn, "location")) {
1369 if (pn.getChild("var") != null) {
1370 // should be changed into a namespace check */
1371 return new VarExpr(pn.getChild("var").getTerminal());
1372 } else if (pn.getChild("cast") != null) {
1373 return parse_cast(pn.getChild("cast"));
1374 } else if (pn.getChild("dot") != null) {
1375 return parse_dot(pn.getChild("dot"));
1377 throw new IRException();
1381 private RelationExpr parse_relation(ParseNode pn) {
1382 if (!precheck(pn, "relation")) {
1386 String relname = pn.getChild("name").getTerminal();
1387 boolean inverse = pn.getChild("inv") == null;
1388 Expr expr = parse_expr(pn.getChild("expr"));
1394 RelationDescriptor relation = lookupRelation(relname);
1396 if (relation == null) {
1397 /* Semantic Error: relation not definied" */
1398 er.report(pn, "Undefined relation '" + relname + "'");
1402 /* add usage so correct sets are created */
1403 relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1405 return new RelationExpr(expr, relation, inverse);
1408 private SizeofExpr parse_sizeof(ParseNode pn) {
1409 if (!precheck(pn, "sizeof")) {
1414 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1416 if (setexpr == null) {
1420 return new SizeofExpr(setexpr);
1423 private CastExpr parse_cast(ParseNode pn) {
1424 if (!precheck(pn, "cast")) {
1429 String typename = pn.getChild("type").getTerminal();
1430 assert typename != null;
1431 TypeDescriptor type = lookupType(typename);
1434 /* semantic error: undefined type in cast */
1435 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1440 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1446 return new CastExpr(type, expr);
1449 private SetExpr parse_setexpr(ParseNode pn) {
1450 if (!precheck(pn, "setexpr")) {
1454 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1456 if (pn.getChild("set") != null) {
1457 String setname = pn.getChild("set").getTerminal();
1458 assert setname != null;
1459 SetDescriptor sd = lookupSet(setname);
1462 er.report(pn, "Unknown or undefined set '" + setname + "'");
1465 return new SetExpr(sd);
1467 } else if (pn.getChild("dot") != null) {
1468 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1469 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1470 relation.addUsage(RelationDescriptor.IMAGE);
1471 return new ImageSetExpr(vd, relation);
1472 } else if (pn.getChild("dotinv") != null) {
1473 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1474 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1475 relation.addUsage(RelationDescriptor.INVIMAGE);
1476 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1478 throw new IRException();
1482 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1483 if (!precheck(pn, "quantifiervar")) {
1488 String varname = pn.getTerminal();
1489 assert varname != null;
1491 /* NOTE: quantifier var's are only found in the constraints and
1492 model definitions... therefore we can do a semantic check here
1493 to make sure that the variables exist in the symbol table */
1495 /* NOTE: its assumed that the symbol table stack is appropriately
1496 set up with the parent quantifier symbol table */
1497 assert !sts.empty();
1499 /* do semantic check and if valid, add it to symbol table
1500 and add it to the quantifier as well */
1501 if (sts.peek().contains(varname)) {
1502 return new VarDescriptor(varname);
1504 /* Semantic Error: undefined variable */
1505 er.report(pn, "Undefined variable '" + varname + "'");
1510 private LiteralExpr parse_literal(ParseNode pn) {
1511 if (!precheck(pn, "literal")) {
1515 if (pn.getChild("boolean") != null) {
1516 if (pn.getChild("boolean").getChild("true") != null) {
1517 return new BooleanLiteralExpr(true);
1519 return new BooleanLiteralExpr(false);
1521 } else if (pn.getChild("decimal") != null) {
1522 String integer = pn.getChild("decimal").getTerminal();
1524 /* Check for integer literal overflow */
1525 BigInteger intLitBI = new BigInteger(integer);
1526 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1527 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1530 if (intLitBI.compareTo(intMin) < 0) {
1531 value = Integer.MIN_VALUE;
1532 er.warn(pn, "Integer literal overflow");
1533 } else if (intLitBI.compareTo(intMax) > 0) {
1534 value = Integer.MAX_VALUE;
1535 er.warn(pn, "Integer literal overflow");
1537 /* no truncation needed */
1538 value = Integer.parseInt(integer);
1541 return new IntegerLiteralExpr(value);
1542 } else if (pn.getChild("token") != null) {
1543 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1544 } else if (pn.getChild("string") != null) {
1545 throw new IRException("string unsupported");
1546 } else if (pn.getChild("char") != null) {
1547 throw new IRException("char unsupported");
1549 throw new IRException("unknown literal expression type.");
1553 private OpExpr parse_operator(ParseNode pn) {
1554 if (!precheck(pn, "operator")) {
1558 String opname = pn.getChild("op").getTerminal();
1559 Opcode opcode = Opcode.decodeFromString(opname);
1561 if (opcode == null) {
1562 er.report(pn, "Unsupported operation: " + opname);
1566 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1569 if (pn.getChild("right") != null) {
1570 right = parse_expr(pn.getChild("right").getChild("expr"));
1577 if (right == null && opcode != Opcode.NOT) {
1578 er.report(pn, "Two arguments required.");
1582 return new OpExpr(opcode, left, right);
1585 private DotExpr parse_dot(ParseNode pn) {
1586 if (!precheck(pn, "dot")) {
1590 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1596 String field = pn.getChild("field").getTerminal();
1600 if (pn.getChild("index") != null) {
1601 index = parse_expr(pn.getChild("index").getChild("expr"));
1603 if (index == null) {
1608 return new DotExpr(left, field, index);