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?) */
393 Iterator consiterator = state.vConstraints.iterator();
395 while (consiterator.hasNext()) {
396 Constraint cons = (Constraint) consiterator.next();
398 final SymbolTable consst = cons.getSymbolTable();
399 SemanticAnalyzer sa = new SemanticAnalyzer() {
400 public IRErrorReporter getErrorReporter() { return er; }
401 public SymbolTable getSymbolTable() { return consst; }
404 TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
406 if (constype == null) {
408 } else if (constype != ReservedTypeDescriptor.INT) {
409 er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
417 private boolean parse_constraint(ParseNode pn) {
418 if (!precheck(pn, "constraint")) {
423 Constraint constraint = new Constraint();
426 boolean crash = pn.getChild("crash") != null;
427 constraint.setCrash(crash);
429 /* set up symbol table for constraint */
431 sts.push(constraint.getSymbolTable());
433 /* get quantifiers */
434 if (pn.getChild("quantifiers") != null) {
435 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
437 for (int i = 0; i < quantifiers.size(); i++) {
438 ParseNode qn = quantifiers.elementAt(i);
439 assert qn.getLabel().equals("quantifier");
440 Quantifier quantifier = parse_quantifier(qn);
441 if (quantifier == null) {
444 constraint.addQuantifier(quantifier);
450 LogicStatement logicexpr = parse_body(pn.getChild("body"));
452 if (logicexpr == null) {
455 constraint.setLogicStatement(logicexpr);
458 /* pop symbol table stack */
459 SymbolTable st = sts.pop();
461 /* make sure the stack we pop is our constraint s.t. */
462 assert st == constraint.getSymbolTable();
465 /* add to vConstraints */
466 vConstraints.addElement(constraint);
471 private Quantifier parse_quantifier(ParseNode pn) {
472 if (!precheck(pn, "quantifier")) {
476 if (pn.getChild("forall") != null) { /* forall element in Set */
477 SetQuantifier sq = new SetQuantifier();
480 VarDescriptor vd = reserveName(pn.getChild("var"));
489 SetDescriptor set = parse_set(pn.getChild("set"));
494 vd.setType(set.getType());
496 /* return to caller */
499 } else if (pn.getChild("relation") != null) { /* for < v1, v2 > in Relation */
500 RelationQuantifier rq = new RelationQuantifier();
503 VarDescriptor vd1 = reserveName(pn.getChild("left"));
504 VarDescriptor vd2 = reserveName(pn.getChild("right"));
506 if ((vd1 == null) || (vd2 == null)) {
510 rq.setTuple(vd1, vd2);
513 String relationname = pn.getChild("relation").getTerminal();
514 assert relationname != null;
515 RelationDescriptor rd = lookupRelation(relationname);
522 vd1.setType(rd.getDomain().getType());
523 vd1.setSet(rd.getDomain());
524 vd2.setType(rd.getRange().getType());
525 vd2.setSet(rd.getRange());
527 } else if (pn.getChild("for") != null) { /* for j = x to y */
528 ForQuantifier fq = new ForQuantifier();
531 VarDescriptor vd = reserveName(pn.getChild("var"));
537 vd.setSet(lookupSet("int", false));
538 vd.setType(ReservedTypeDescriptor.INT);
541 /* grab lower/upper bounds */
542 Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
543 Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
546 if ((lower == null) || (upper == null)) {
549 vd.setBounds(lower,upper);
550 fq.setBounds(lower, upper);
554 throw new IRException("not supported yet");
558 private LogicStatement parse_body(ParseNode pn) {
559 if (!precheck(pn, "body")) {
563 if (pn.getChild("and") != null) {
565 LogicStatement left, right;
566 left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
567 right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
569 if ((left == null) || (right == null)) {
573 // what do we want to call the and/or/not body classes?
574 return new LogicStatement(LogicStatement.AND, left, right);
575 } else if (pn.getChild("or") != null) {
577 LogicStatement left, right;
578 left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
579 right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
581 if ((left == null) || (right == null)) {
585 return new LogicStatement(LogicStatement.OR, left, right);
586 } else if (pn.getChild("not") != null) {
588 LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
594 return new LogicStatement(LogicStatement.NOT, left);
595 } else if (pn.getChild("predicate") != null) {
596 return parse_predicate(pn.getChild("predicate"));
598 throw new IRException();
602 private Predicate parse_predicate(ParseNode pn) {
603 if (!precheck(pn, "predicate")) {
607 if (pn.getChild("inclusion") != null) {
608 ParseNode in = pn.getChild("inclusion");
611 Expr expr = parse_expr(in.getChild("expr"));
618 SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
620 if (setexpr == null) {
624 return new InclusionPredicate(expr, setexpr);
625 } else if (pn.getChild("expr") != null) {
626 Expr expr = parse_expr(pn.getChild("expr"));
632 return new ExprPredicate(expr);
634 throw new IRException();
638 private SetDescriptor parse_set(ParseNode pn) {
639 if (!precheck(pn, "set")) {
643 if (pn.getChild("name") != null) {
644 String setname = pn.getChild("name").getTerminal();
645 assert setname != null;
647 if (!stSets.contains(setname)) {
648 /* Semantic Error: unknown set */
649 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
652 /* all good, get setdescriptor */
653 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
657 } else if (pn.getChild("listofliterals") != null) {
658 TokenSetDescriptor tokenset = new TokenSetDescriptor();
659 ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
660 assert token_literals.size() > 0;
662 for (int i = 0; i < token_literals.size(); i++) {
663 ParseNode literal = token_literals.elementAt(i);
664 assert literal.getLabel().equals("literal");
665 LiteralExpr litexpr = parse_literal(literal);
667 if (litexpr == null) {
671 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
672 tokenset.addLiteral(litexpr);
674 er.report(literal, "Elements of a user-defined set must be of type token or integer");
675 // return null; /* don't think we need to return null */
681 throw new IRException(pn.getTerminal());
685 private boolean parse_space(ParseNode pn) {
686 if (!precheck(pn, "space")) {
691 ParseNodeVector sets = pn.getChildren("setdefinition");
692 ParseNodeVector relations = pn.getChildren("relationdefinition");
694 assert pn.getChildren().size() == (sets.size() + relations.size());
697 for (int i = 0; i < sets.size(); i++) {
698 if (!parse_setdefinition(sets.elementAt(i))) {
703 /* parse relations */
704 for (int i = 0; i < relations.size(); i++) {
705 if (!parse_relationdefinition(relations.elementAt(i))) {
710 // ok, all the spaces have been parsed, now we should typecheck and check
713 // #TBD#: typecheck and check for cycles
715 /* replace missing with actual */
716 Iterator allsets = state.stSets.descriptors();
718 while (allsets.hasNext()) {
719 SetDescriptor sd = (SetDescriptor) allsets.next();
720 Vector subsets = sd.getSubsets();
722 for (int i = 0; i < subsets.size(); i++) {
723 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
725 if (subset instanceof MissingSetDescriptor) {
726 SetDescriptor newsubset = lookupSet(subset.getSymbol());
728 if (newsubset == null) {
729 er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
731 subsets.setElementAt(newsubset, i);
740 private boolean parse_setdefinition(ParseNode pn) {
741 if (!precheck(pn, "setdefinition")) {
748 String setname = pn.getChild("name").getTerminal();
749 assert (setname != null);
751 SetDescriptor sd = new SetDescriptor(setname);
754 String settype = pn.getChild("type").getTerminal();
755 TypeDescriptor type = lookupType(settype);
757 er.report(pn, "Undefined type '" + settype + "'");
763 /* is this a partition? */
764 boolean partition = pn.getChild("partition") != null;
765 sd.isPartition(partition);
767 /* if set has subsets, add them to set descriptor */
768 if (pn.getChild("setlist") != null) {
769 ParseNodeVector setlist = pn.getChild("setlist").getChildren();
771 for (int i = 0; i < setlist.size(); i++) {
772 String subsetname = setlist.elementAt(i).getLabel();
773 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
777 /* add set to symbol table */
778 if (stSets.contains(setname)) {
779 // Semantic Check: redefinition
780 er.report(pn, "Redefinition of set: " + setname);
789 private boolean parse_relationdefinition(ParseNode pn) {
790 if (!precheck(pn, "relationdefinition")) {
796 /* get relation name */
797 String relname = pn.getChild("name").getTerminal();
798 assert relname != null;
800 RelationDescriptor rd = new RelationDescriptor(relname);
802 /* check if static */
803 boolean bStatic = pn.getChild("static") != null;
804 rd.isStatic(bStatic);
807 String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
808 assert domainsetname != null;
811 String rangesetname = pn.getChild("range").getChild("type").getTerminal();
812 assert rangesetname != null;
814 /* get domain multiplicity */
816 if (pn.getChild("domain").getChild("domainmult") != null)
817 domainmult = pn.getChild("domain").getChild("domainmult").getChild("mult").getTerminal();
818 //assert domainmult != null;
820 /* get range multiplicity */
822 if (pn.getChild("range").getChild("domainrange") != null)
823 rangemult = pn.getChild("range").getChild("domainrange").getChild("mult").getTerminal();
824 //assert rangemult != null;
826 /* NOTE: it is assumed that the sets have been parsed already so that the
827 set namespace is fully populated. any missing setdescriptors for the set
828 symbol table will be assumed to be errors and reported. */
830 SetDescriptor domainset = lookupSet(domainsetname);
831 if (domainset == null) {
832 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
835 rd.setDomain(domainset);
838 SetDescriptor rangeset = lookupSet(rangesetname);
839 if (rangeset == null) {
840 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
843 rd.setRange(rangeset);
846 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
848 /* lets add the relation to the global symbol table */
849 if (!stRelations.contains(relname)) {
852 er.report(pn, "Redefinition of relation '" + relname + "'");
859 private boolean parse_structures(ParseNode pn) {
860 if (!precheck(pn, "structures")) {
865 ParseNodeVector structures = pn.getChildren("structure");
867 for (int i = 0; i < structures.size(); i++) {
868 if (!parse_structure(structures.elementAt(i))) {
873 ParseNodeVector globals = pn.getChildren("global");
875 for (int i = 0; i < globals.size(); i++) {
876 if (!parse_global(globals.elementAt(i))) {
881 // ok, all the structures have been parsed, now we gotta type check
883 Enumeration types = stTypes.getDescriptors();
884 while (types.hasMoreElements()) {
885 TypeDescriptor t = (TypeDescriptor) types.nextElement();
887 if (t instanceof ReservedTypeDescriptor) {
888 // we don't need to check reserved types
889 } else if (t instanceof StructureTypeDescriptor) {
891 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
892 TypeDescriptor subtype = type.getSuperType();
894 // check that the subtype is valid
895 if (subtype instanceof MissingTypeDescriptor) {
896 TypeDescriptor newtype = lookupType(subtype.getSymbol());
897 if (newtype == null) {
898 // subtype not defined anywheere
899 // #TBD#: somehow determine how we can get the original parsenode (global function?)
900 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
903 type.setSuperType(newtype);
907 Iterator fields = type.getFields();
909 while (fields.hasNext()) {
910 FieldDescriptor field = (FieldDescriptor) fields.next();
911 TypeDescriptor fieldtype = field.getType();
913 assert fieldtype != null;
915 // check that the type is valid
916 if (fieldtype instanceof MissingTypeDescriptor) {
917 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
918 if (newtype == null) {
919 // type never defined
920 // #TBD#: replace new ParseNode with original parsenode
921 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
924 assert newtype != null;
925 field.setType(newtype);
930 Iterator labels = type.getLabels();
932 while (labels.hasNext()) {
933 LabelDescriptor label = (LabelDescriptor) labels.next();
934 TypeDescriptor labeltype = label.getType();
936 assert labeltype != null;
938 // check that the type is valid
939 if (labeltype instanceof MissingTypeDescriptor) {
940 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
941 if (newtype == null) {
942 // type never defined
943 // #TBD#: replace new ParseNode with original parsenode
944 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
947 assert newtype != null;
948 label.setType(newtype);
954 throw new IRException("shouldn't be any other typedescriptor classes");
962 types = stTypes.getDescriptors();
964 while (types.hasMoreElements()) {
965 TypeDescriptor t = (TypeDescriptor) types.nextElement();
967 if (t instanceof ReservedTypeDescriptor) {
968 // we don't need to check reserved types
969 } else if (t instanceof StructureTypeDescriptor) {
971 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
972 TypeDescriptor subtype = type.getSuperType();
973 Iterator fields = type.getFields();
975 while (fields.hasNext()) {
976 FieldDescriptor field = (FieldDescriptor) fields.next();
978 if (field instanceof ArrayDescriptor) {
979 ArrayDescriptor ad = (ArrayDescriptor) field;
980 Expr indexbound = ad.getIndexBound();
981 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
982 public IRErrorReporter getErrorReporter() { return er; }
983 public SymbolTable getSymbolTable() { return stGlobals; }
986 if (indextype == null) {
988 } else if (indextype != ReservedTypeDescriptor.INT) {
989 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
995 Iterator labels = type.getLabels();
997 while (labels.hasNext()) {
998 LabelDescriptor label = (LabelDescriptor) labels.next();
999 Expr index = label.getIndex();
1001 if (index != null) {
1002 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
1003 public IRErrorReporter getErrorReporter() { return er; }
1004 public SymbolTable getSymbolTable() { return stGlobals; }
1007 if (indextype != ReservedTypeDescriptor.INT) {
1008 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
1014 throw new IRException("shouldn't be any other typedescriptor classes");
1018 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
1019 // subtypes, of course, are not real subtypes, they are merely a way to validate a
1025 private boolean parse_global(ParseNode pn) {
1026 if (!precheck(pn, "global")) {
1030 String name = pn.getChild("name").getTerminal();
1031 assert name != null;
1033 String type = pn.getChild("type").getTerminal();
1034 assert type != null;
1035 TypeDescriptor td = lookupType(type);
1037 assert !(td instanceof ReservedTypeDescriptor);
1039 if (stGlobals.contains(name)) {
1040 /* redefinition of global */
1041 er.report(pn, "Redefinition of global '" + name + "'");
1045 stGlobals.add(new VarDescriptor(name, name, td,true));
1049 private boolean parse_structure(ParseNode pn) {
1050 if (!precheck(pn, "structure")) {
1055 String typename = pn.getChild("name").getTerminal();
1056 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1058 if (pn.getChild("subtype") != null) {
1059 // has a subtype, lets try to resolve it
1060 String subtype = pn.getChild("subtype").getTerminal();
1062 if (subtype.equals(typename)) {
1063 // Semantic Error: cyclic inheritance
1064 er.report(pn, "Cyclic inheritance prohibited");
1068 /* lookup the type to get the type descriptor */
1069 type.setSuperType(lookupType(subtype, CREATE_MISSING));
1072 // set the current type so that the recursive parses on the labels
1073 // and fields can add themselves automatically to the current type
1074 dCurrentType = type;
1076 // parse the labels and fields
1077 if (!parse_labelsandfields(pn.getChild("lf"))) {
1081 if (stTypes.contains(typename)) {
1082 er.report(pn, "Redefinition of type '" + typename + "'");
1091 private boolean parse_labelsandfields(ParseNode pn) {
1092 if (!precheck(pn, "lf")) {
1098 // check the fields first (need the field names
1099 // to type check the labels)
1100 if (!parse_fields(pn.getChild("fields"))) {
1104 // check the labels now that all the fields are sorted
1105 if (!parse_labels(pn.getChild("labels"))) {
1112 private boolean parse_fields(ParseNode pn) {
1113 if (!precheck(pn, "fields")) {
1119 /* NOTE: because the order of the fields is important when defining a data structure,
1120 and because the order is defined by the order of the fields defined in the field
1121 vector, its important that the parser returns the fields in the correct order */
1123 ParseNodeVector fields = pn.getChildren();
1125 for (int i = 0; i < fields.size(); i++) {
1126 ParseNode field = fields.elementAt(i);
1131 if (field.getChild("reserved") != null) {
1133 // #TBD#: it will be necessary for reserved field descriptors to generate
1134 // a unique symbol for the type descriptor requires it for its hashtable
1135 fd = new ReservedFieldDescriptor();
1138 name = field.getChild("name").getTerminal();
1139 fd = new FieldDescriptor(name);
1143 String type = field.getChild("type").getTerminal();
1144 boolean ptr = field.getChild("*") != null;
1147 fd.setType(lookupType(type, CREATE_MISSING));
1149 if (field.getChild("index") != null) {
1150 // field is an array, so create an array descriptor to wrap the
1151 // field descriptor and then replace the top level field descriptor with
1152 // this array descriptor
1153 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1155 // #ATTN#: do we really want to return an exception here?
1156 throw new IRException("invalid index expression");
1158 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1162 // add the current field to the current type
1163 if (reserved == false) {
1164 // lets double check that we are redefining a field
1165 if (dCurrentType.getField(name) != null) {
1166 // Semantic Error: field redefinition
1167 er.report(pn, "Redefinition of field '" + name + "'");
1170 dCurrentType.addField(fd);
1173 dCurrentType.addField(fd);
1180 private boolean parse_labels(ParseNode pn) {
1181 if (!precheck(pn, "labels")) {
1187 /* NOTE: parse_labels should be called after the fields have been parsed because any
1188 labels not found in the field set of the current type will be flagged as errors */
1190 ParseNodeVector labels = pn.getChildren();
1192 for (int i = 0; i < labels.size(); i++) {
1193 ParseNode label = labels.elementAt(i);
1194 String name = label.getChild("name").getTerminal();
1195 LabelDescriptor ld = new LabelDescriptor(name);
1197 if (label.getChild("index") != null) {
1198 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1200 /* #ATTN#: do we really want to return an exception here? */
1201 throw new IRException("Invalid expression");
1206 String type = label.getChild("type").getTerminal();
1208 ld.setType(lookupType(type, CREATE_MISSING));
1210 String field = label.getChild("field").getTerminal();
1211 FieldDescriptor fd = dCurrentType.getField(field);
1214 /* Semantic Error: Undefined field in label */
1215 er.report(label, "Undefined field '" + field + "' in label");
1221 /* add label to current type */
1222 if (dCurrentType.getLabel(name) != null) {
1223 /* semantic error: label redefinition */
1224 er.report(pn, "Redefinition of label '" + name + "'");
1227 dCurrentType.addLabel(ld);
1234 private Expr parse_expr(ParseNode pn) {
1235 if (!precheck(pn, "expr")) {
1239 if (pn.getChild("var") != null) {
1240 // we've got a variable reference... we'll have to scope check it later
1241 // when we are completely done... there are also some issues of cyclic definitions
1242 return new VarExpr(pn.getChild("var").getTerminal());
1243 } else if (pn.getChild("literal") != null) {
1244 return parse_literal(pn.getChild("literal"));
1245 } else if (pn.getChild("operator") != null) {
1246 return parse_operator(pn.getChild("operator"));
1247 } else if (pn.getChild("relation") != null) {
1248 return parse_relation(pn.getChild("relation"));
1249 } else if (pn.getChild("sizeof") != null) {
1250 return parse_sizeof(pn.getChild("sizeof"));
1251 } else if (pn.getChild("simple_expr") != null) {
1252 return parse_simple_expr(pn.getChild("simple_expr"));
1253 } else if (pn.getChild("elementof") != null) {
1254 return parse_elementof(pn.getChild("elementof"));
1255 } else if (pn.getChild("tupleof") != null) {
1256 return parse_tupleof(pn.getChild("tupleof"));
1257 } else if (pn.getChild("isvalid") != null) {
1258 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1261 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1266 private Expr parse_elementof(ParseNode pn) {
1267 if (!precheck(pn, "elementof")) {
1272 String setname = pn.getChild("name").getTerminal();
1273 assert setname != null;
1274 SetDescriptor sd = lookupSet(setname);
1277 er.report(pn, "Undefined set '" + setname + "'");
1281 /* get left side expr */
1282 Expr expr = parse_expr(pn.getChild("expr"));
1288 return new ElementOfExpr(expr, sd);
1291 private Expr parse_tupleof(ParseNode pn) {
1292 if (!precheck(pn, "tupleof")) {
1297 String relname = pn.getChild("name").getTerminal();
1298 assert relname != null;
1299 RelationDescriptor rd = lookupRelation(relname);
1302 er.report(pn, "Undefined relation '" + relname + "'");
1306 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1307 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1309 if ((left == null) || (right == null)) {
1313 return new TupleOfExpr(left, right, rd);
1316 private Expr parse_simple_expr(ParseNode pn) {
1317 if (!precheck(pn, "simple_expr")) {
1321 // only locations so far
1322 return parse_location(pn.getChild("location"));
1325 private Expr parse_location(ParseNode pn) {
1326 if (!precheck(pn, "location")) {
1330 if (pn.getChild("var") != null) {
1331 // should be changed into a namespace check */
1332 return new VarExpr(pn.getChild("var").getTerminal());
1333 } else if (pn.getChild("cast") != null) {
1334 return parse_cast(pn.getChild("cast"));
1335 } else if (pn.getChild("dot") != null) {
1336 return parse_dot(pn.getChild("dot"));
1338 throw new IRException();
1342 private RelationExpr parse_relation(ParseNode pn) {
1343 if (!precheck(pn, "relation")) {
1347 String relname = pn.getChild("name").getTerminal();
1348 boolean inverse = pn.getChild("inv") != null;
1349 Expr expr = parse_expr(pn.getChild("expr"));
1355 RelationDescriptor relation = lookupRelation(relname);
1357 if (relation == null) {
1358 /* Semantic Error: relation not definied" */
1359 er.report(pn, "Undefined relation '" + relname + "'");
1363 /* add usage so correct sets are created */
1364 relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1366 return new RelationExpr(expr, relation, inverse);
1369 private SizeofExpr parse_sizeof(ParseNode pn) {
1370 if (!precheck(pn, "sizeof")) {
1375 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1377 if (setexpr == null) {
1381 return new SizeofExpr(setexpr);
1384 private CastExpr parse_cast(ParseNode pn) {
1385 if (!precheck(pn, "cast")) {
1390 String typename = pn.getChild("type").getTerminal();
1391 assert typename != null;
1392 TypeDescriptor type = lookupType(typename);
1395 /* semantic error: undefined type in cast */
1396 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1401 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1407 return new CastExpr(type, expr);
1410 private SetExpr parse_setexpr(ParseNode pn) {
1411 if (!precheck(pn, "setexpr")) {
1415 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1417 if (pn.getChild("set") != null) {
1418 String setname = pn.getChild("set").getTerminal();
1419 assert setname != null;
1420 SetDescriptor sd = lookupSet(setname);
1423 er.report(pn, "Unknown or undefined set '" + setname + "'");
1426 return new SetExpr(sd);
1428 } else if (pn.getChild("dot") != null) {
1429 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1430 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1431 relation.addUsage(RelationDescriptor.IMAGE);
1432 return new ImageSetExpr(vd, relation);
1433 } else if (pn.getChild("dotinv") != null) {
1434 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1435 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1436 relation.addUsage(RelationDescriptor.INVIMAGE);
1437 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1439 throw new IRException();
1443 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1444 if (!precheck(pn, "quantifiervar")) {
1449 String varname = pn.getTerminal();
1450 assert varname != null;
1452 /* NOTE: quantifier var's are only found in the constraints and
1453 model definitions... therefore we can do a semantic check here
1454 to make sure that the variables exist in the symbol table */
1456 /* NOTE: its assumed that the symbol table stack is appropriately
1457 set up with the parent quantifier symbol table */
1458 assert !sts.empty();
1460 /* do semantic check and if valid, add it to symbol table
1461 and add it to the quantifier as well */
1462 if (sts.peek().contains(varname)) {
1463 VarDescriptor vdold=(VarDescriptor)sts.peek().get(varname);
1465 /* Dan was creating a new VarDescriptor...This seems
1466 like the wrong thing to do. We'll just lookup the
1468 --------------------------------------------------
1469 VarDescriptor vd=new VarDescriptor(varname);
1470 vd.setSet(vdold.getSet()); return vd;*/
1472 /* Semantic Error: undefined variable */
1473 er.report(pn, "Undefined variable '" + varname + "'");
1478 private LiteralExpr parse_literal(ParseNode pn) {
1479 if (!precheck(pn, "literal")) {
1483 if (pn.getChild("boolean") != null) {
1484 if (pn.getChild("boolean").getChild("true") != null) {
1485 return new BooleanLiteralExpr(true);
1487 return new BooleanLiteralExpr(false);
1489 } else if (pn.getChild("decimal") != null) {
1490 String integer = pn.getChild("decimal").getTerminal();
1492 /* Check for integer literal overflow */
1493 BigInteger intLitBI = new BigInteger(integer);
1494 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1495 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1498 if (intLitBI.compareTo(intMin) < 0) {
1499 value = Integer.MIN_VALUE;
1500 er.warn(pn, "Integer literal overflow");
1501 } else if (intLitBI.compareTo(intMax) > 0) {
1502 value = Integer.MAX_VALUE;
1503 er.warn(pn, "Integer literal overflow");
1505 /* no truncation needed */
1506 value = Integer.parseInt(integer);
1509 return new IntegerLiteralExpr(value);
1510 } else if (pn.getChild("token") != null) {
1511 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1512 } else if (pn.getChild("string") != null) {
1513 throw new IRException("string unsupported");
1514 } else if (pn.getChild("char") != null) {
1515 throw new IRException("char unsupported");
1517 throw new IRException("unknown literal expression type.");
1521 private OpExpr parse_operator(ParseNode pn) {
1522 if (!precheck(pn, "operator")) {
1526 String opname = pn.getChild("op").getTerminal();
1527 Opcode opcode = Opcode.decodeFromString(opname);
1529 if (opcode == null) {
1530 er.report(pn, "Unsupported operation: " + opname);
1534 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1537 if (pn.getChild("right") != null) {
1538 right = parse_expr(pn.getChild("right").getChild("expr"));
1545 if (right == null && opcode != Opcode.NOT) {
1546 er.report(pn, "Two arguments required.");
1550 return new OpExpr(opcode, left, right);
1553 private DotExpr parse_dot(ParseNode pn) {
1554 if (!precheck(pn, "dot")) {
1558 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1564 String field = pn.getChild("field").getTerminal();
1568 if (pn.getChild("index") != null) {
1569 index = parse_expr(pn.getChild("index").getChild("expr"));
1571 if (index == null) {
1576 return new DotExpr(left, field, index);