4 import java.math.BigInteger;
8 public class SemanticChecker {
10 private static final boolean CREATE_MISSING = true;
20 SymbolTable stRelations;
22 SymbolTable stGlobals;
24 StructureTypeDescriptor dCurrentType;
28 public SemanticChecker () {
34 public boolean check(State state, IRErrorReporter er) {
37 State.currentState = state;
40 throw new IRException("IRBuilder.build: Received null ErrorReporter");
45 if (state.ptStructures == null) {
46 throw new IRException("IRBuilder.build: Received null ParseNode");
49 state.vConstraints = new Vector();
50 vConstraints = state.vConstraints;
52 state.vRules = new Vector();
53 vRules = state.vRules;
55 state.stTypes = new SymbolTable();
56 stTypes = state.stTypes;
58 state.stSets = new SymbolTable();
59 stSets = state.stSets;
61 state.stRelations = new SymbolTable();
62 stRelations = state.stRelations;
64 state.stGlobals = new SymbolTable();
65 stGlobals = state.stGlobals;
67 sts = new SymbolTableStack();
69 // add int and bool to the types list
70 stTypes.add(ReservedTypeDescriptor.BIT);
71 stTypes.add(ReservedTypeDescriptor.BYTE);
72 stTypes.add(ReservedTypeDescriptor.SHORT);
73 stTypes.add(ReservedTypeDescriptor.INT);
75 stSets.add(new ReservedSetDescriptor("int", ReservedTypeDescriptor.INT));
76 stSets.add(new ReservedSetDescriptor("token", ReservedTypeDescriptor.INT));
80 er.setFilename(state.infile + ".struct");
81 if (!parse_structures(state.ptStructures)) {
84 er.report(null, "Error parsing structs.");
87 er.setFilename(state.infile + ".space");
88 if (!parse_space(state.ptSpace)) {
90 er.report(null, "Error parsing sets and relations.");
93 er.setFilename(state.infile + ".constraints");
94 if (!parse_constraints(state.ptConstraints)) {
96 er.report(null, "Error parsing constraints.");
99 er.setFilename(state.infile + ".model");
100 if (!parse_rules(state.ptModel)) {
102 er.report(null, "Error parsing model definition rules.");
108 /********************** HELPER FUNCTIONS ************************/
111 * special case lookup that returns null if no such type exists
113 private TypeDescriptor lookupType(String typename) {
114 return lookupType(typename, false);
118 * does a look up in the types symbol table. if the type is
119 * not found than a missing type descriptor is returned
121 private TypeDescriptor lookupType(String typename, boolean createmissing) {
122 if (stTypes.get(typename) != null) {
123 // the type exists, so plug in the descriptor directly
124 return (TypeDescriptor) stTypes.get(typename);
125 } else if (createmissing) {
126 return new MissingTypeDescriptor(typename);
135 private VarDescriptor reserveName(ParseNode pn) {
137 String varname = pn.getTerminal();
138 assert varname != null;
140 /* do semantic check and if valid, add it to symbol table
141 and add it to the quantifier as well */
142 if (sts.peek().contains(varname)) {
143 /* Semantic Error: redefinition */
144 er.report(pn, "Redefinition of '" + varname + "'");
147 VarDescriptor vd = new VarDescriptor(varname);
154 * special case lookup that returns null if no such set exists
156 private SetDescriptor lookupSet(String setname) {
157 return lookupSet(setname, false);
161 * does a look up in the set's symbol table. if the set is
162 * not found than a missing set descriptor is returned
164 private SetDescriptor lookupSet(String setname, boolean createmissing) {
165 if (stSets.get(setname) != null) {
166 // the set exists, so plug in the descriptor directly
167 return (SetDescriptor) stSets.get(setname);
168 } else if (createmissing) {
169 return new MissingSetDescriptor(setname);
176 * does a look up in the set's symbol table. if the set is
177 * not found than a missing set descriptor is returned
179 private RelationDescriptor lookupRelation(String relname) {
180 if (stRelations.get(relname) != null) {
181 // the relation exists, so plug in the descriptor directly
182 return (RelationDescriptor) stRelations.get(relname);
189 private static int count = 0;
190 private boolean precheck(ParseNode pn, String label) {
192 er.report(pn, "IE: Expected '" + label + "', got null");
197 if (! pn.getLabel().equals(label)) {
198 er.report(pn, "IE: Expected '" + label + "', got '" + pn.getLabel() + "'");
203 if (state.verbose >= 2) {
204 System.err.println("visiting*" + (count++) + ": " + label);
210 /********************* PARSING FUNCTIONS ************************/
212 private boolean parse_rules(ParseNode pn) {
213 if (!precheck(pn, "rules")) {
218 ParseNodeVector rules = pn.getChildren();
220 for (int i = 0; i < rules.size(); i++) {
221 ParseNode rule = rules.elementAt(i);
222 if (!parse_rule(rule)) {
223 er.report(rule, "Error parsing rule");
229 Iterator ruleiterator = state.vRules.iterator();
231 while (ruleiterator.hasNext()) {
232 Rule rule = (Rule) ruleiterator.next();
233 Expr guard = rule.getGuardExpr();
234 final SymbolTable rulest = rule.getSymbolTable();
235 SemanticAnalyzer sa = new SemanticAnalyzer() {
236 public IRErrorReporter getErrorReporter() { return er; }
237 public SymbolTable getSymbolTable() { return rulest; }
239 TypeDescriptor guardtype = guard.typecheck(sa);
241 if (guardtype == null) {
243 } else if (guardtype != ReservedTypeDescriptor.INT) {
244 er.report(null, "Type of guard must be 'int' not '" + guardtype.getSymbol() + "'");
248 if (!rule.getInclusion().typecheck(sa)) {
249 er.report(null, "Error typechecking rule:"+rule);
253 Iterator quantifiers = rule.quantifiers();
255 while (quantifiers.hasNext()) {
256 Quantifier q = (Quantifier) quantifiers.next();
258 if (q instanceof ForQuantifier && !((ForQuantifier)q).typecheck(sa)) {
264 /* do any post checks ?? */
269 private boolean parse_rule(ParseNode pn) {
270 if (!precheck(pn, "rule")) {
275 Rule rule = new Rule();
278 boolean isstatic = pn.getChild("static") != null;
279 boolean isdelay = pn.getChild("delay") != null;
280 rule.setStatic(isstatic);
281 rule.setDelay(isdelay);
283 /* set up symbol table for constraint */
286 sts.push(rule.getSymbolTable());
287 /* optional quantifiers */
288 if (pn.getChild("quantifiers") != null) {
289 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
290 for (int i = 0; i < quantifiers.size(); i++) {
291 ParseNode qn = quantifiers.elementAt(i);
292 Quantifier quantifier = parse_quantifier(qn);
294 if (quantifier == null) {
297 rule.addQuantifier(quantifier);
303 Expr guard = parse_expr(pn.getChild("expr"));
308 rule.setGuardExpr(guard);
311 /* inclusion constraint */
312 Inclusion inclusion = parse_inclusion(pn.getChild("inclusion"));
314 if (inclusion == null) {
317 rule.setInclusion(inclusion);
320 /* pop symbol table stack */
321 SymbolTable st = sts.pop();
322 sts.pop(); /* pop off globals */
324 /* make sure the stack we pop is our rule s.t. */
325 assert st == rule.getSymbolTable();
328 /* add rule to global set */
329 vRules.addElement(rule);
334 private Inclusion parse_inclusion(ParseNode pn) {
335 if (!precheck(pn, "inclusion")) {
339 if (pn.getChild("set") != null) {
340 ParseNode set = pn.getChild("set");
341 Expr expr = parse_expr(set.getChild("expr"));
347 String setname = set.getChild("name").getTerminal();
348 assert setname != null;
349 SetDescriptor sd = lookupSet(setname);
352 er.report(set.getChild("name"), "Undefined set '" + setname + "'");
356 return new SetInclusion(expr, sd);
357 } else if (pn.getChild("relation") != null) {
358 ParseNode relation = pn.getChild("relation");
359 Expr leftexpr = parse_expr(relation.getChild("left").getChild("expr"));
360 Expr rightexpr = parse_expr(relation.getChild("right").getChild("expr"));
362 if ((leftexpr == null) || (rightexpr == null)) {
366 String relname = relation.getChild("name").getTerminal();
367 assert relname != null;
368 RelationDescriptor rd = lookupRelation(relname);
371 er.report(relation.getChild("name"), "Undefined relation '" + relname + "'");
375 return new RelationInclusion(leftexpr, rightexpr, rd);
377 throw new IRException();
381 private boolean parse_constraints(ParseNode pn) {
382 if (!precheck(pn, "constraints")) {
385 //System.out.println(pn.PPrint(2,true));
388 ParseNodeVector constraints = pn.getChildren();
390 for (int i = 0; i < constraints.size(); i++) {
391 ParseNode constraint = constraints.elementAt(i);
392 assert constraint.getLabel().equals("constraint");
393 if (!parse_constraint(constraint)) {
398 /* do any post checks... (type constraints, etc?) */
400 Iterator consiterator = state.vConstraints.iterator();
402 while (consiterator.hasNext()) {
403 Constraint cons = (Constraint) consiterator.next();
405 final SymbolTable consst = cons.getSymbolTable();
406 SemanticAnalyzer sa = new SemanticAnalyzer() {
407 public IRErrorReporter getErrorReporter() { return er; }
408 public SymbolTable getSymbolTable() { return consst; }
411 TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
413 if (constype == null) {
414 System.out.println("Failed attempting to type constraint");
416 } else if (constype != ReservedTypeDescriptor.INT) {
417 er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
425 private boolean parse_constraint(ParseNode pn) {
426 if (!precheck(pn, "constraint")) {
431 Constraint constraint = new Constraint();
434 boolean crash = pn.getChild("crash") != null;
435 constraint.setCrash(crash);
437 /* set up symbol table for constraint */
439 sts.push(constraint.getSymbolTable());
441 /* get quantifiers */
442 if (pn.getChild("quantifiers") != null) {
443 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
445 for (int i = 0; i < quantifiers.size(); i++) {
446 ParseNode qn = quantifiers.elementAt(i);
447 assert qn.getLabel().equals("quantifier");
448 Quantifier quantifier = parse_quantifier(qn);
449 if (quantifier == null) {
450 System.out.println("Failed parsing quantifier");
453 constraint.addQuantifier(quantifier);
459 LogicStatement logicexpr = parse_body(pn.getChild("body"));
461 if (logicexpr == null) {
462 System.out.println("Failed parsing logical expression");
465 constraint.setLogicStatement(logicexpr);
468 /* pop symbol table stack */
469 SymbolTable st = sts.pop();
471 /* make sure the stack we pop is our constraint s.t. */
472 assert st == constraint.getSymbolTable();
475 /* add to vConstraints */
476 vConstraints.addElement(constraint);
481 private Quantifier parse_quantifier(ParseNode pn) {
482 if (!precheck(pn, "quantifier")) {
486 if (pn.getChild("forall") != null) { /* forall element in Set */
487 SetQuantifier sq = new SetQuantifier();
490 VarDescriptor vd = reserveName(pn.getChild("var"));
499 SetDescriptor set = parse_set(pn.getChild("set"));
504 vd.setType(set.getType());
506 /* return to caller */
509 } else if (pn.getChild("relation") != null) { /* for < v1, v2 > in Relation */
510 RelationQuantifier rq = new RelationQuantifier();
513 VarDescriptor vd1 = reserveName(pn.getChild("left"));
514 VarDescriptor vd2 = reserveName(pn.getChild("right"));
516 if ((vd1 == null) || (vd2 == null)) {
520 rq.setTuple(vd1, vd2);
523 String relationname = pn.getChild("relation").getTerminal();
524 assert relationname != null;
525 RelationDescriptor rd = lookupRelation(relationname);
531 rd.addUsage(RelationDescriptor.IMAGE);
533 vd1.setType(rd.getDomain().getType());
534 vd1.setSet(rd.getDomain());
535 vd2.setType(rd.getRange().getType());
536 vd2.setSet(rd.getRange());
538 } else if (pn.getChild("for") != null) { /* for j = x to y */
539 ForQuantifier fq = new ForQuantifier();
542 VarDescriptor vd = reserveName(pn.getChild("var"));
548 vd.setSet(lookupSet("int", false));
549 vd.setType(ReservedTypeDescriptor.INT);
552 /* grab lower/upper bounds */
553 Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
554 Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
557 if ((lower == null) || (upper == null)) {
560 vd.setBounds(lower,upper);
561 fq.setBounds(lower, upper);
565 throw new IRException("not supported yet");
569 private LogicStatement parse_body(ParseNode pn) {
570 if (!precheck(pn, "body")) {
574 if (pn.getChild("and") != null) {
576 LogicStatement left, right;
577 left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
578 right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
580 if ((left == null) || (right == null)) {
584 // what do we want to call the and/or/not body classes?
585 return new LogicStatement(LogicStatement.AND, left, right);
586 } else if (pn.getChild("or") != null) {
588 LogicStatement left, right;
589 left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
590 right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
592 if ((left == null) || (right == null)) {
596 return new LogicStatement(LogicStatement.OR, left, right);
597 } else if (pn.getChild("not") != null) {
599 LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
604 return new LogicStatement(LogicStatement.NOT, left);
605 } else if (pn.getChild("predicate") != null) {
606 return parse_predicate(pn.getChild("predicate"));
608 throw new IRException();
612 private Predicate parse_predicate(ParseNode pn) {
613 if (!precheck(pn, "predicate")) {
617 if (pn.getChild("inclusion") != null) {
618 ParseNode in = pn.getChild("inclusion");
621 Expr expr = parse_expr(in.getChild("expr"));
628 SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
630 if (setexpr == null) {
634 return new InclusionPredicate(expr, setexpr);
635 } else if (pn.getChild("expr") != null) {
636 Expr expr = parse_expr(pn.getChild("expr"));
642 return new ExprPredicate(expr);
644 throw new IRException();
648 private SetDescriptor parse_set(ParseNode pn) {
649 if (!precheck(pn, "set")) {
653 if (pn.getChild("name") != null) {
654 String setname = pn.getChild("name").getTerminal();
655 assert setname != null;
657 if (!stSets.contains(setname)) {
658 /* Semantic Error: unknown set */
659 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
662 /* all good, get setdescriptor */
663 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
667 } else if (pn.getChild("listofliterals") != null) {
668 TokenSetDescriptor tokenset = new TokenSetDescriptor();
669 ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
670 assert token_literals.size() > 0;
672 for (int i = 0; i < token_literals.size(); i++) {
673 ParseNode literal = token_literals.elementAt(i);
674 assert literal.getLabel().equals("literal");
675 LiteralExpr litexpr = parse_literal(literal);
677 if (litexpr == null) {
681 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
682 tokenset.addLiteral(litexpr);
684 er.report(literal, "Elements of a user-defined set must be of type token or integer");
685 // return null; /* don't think we need to return null */
691 throw new IRException(pn.getTerminal());
695 private boolean parse_space(ParseNode pn) {
696 if (!precheck(pn, "space")) {
701 ParseNodeVector sets = pn.getChildren("setdefinition");
702 ParseNodeVector relations = pn.getChildren("relationdefinition");
704 assert pn.getChildren().size() == (sets.size() + relations.size());
707 for (int i = 0; i < sets.size(); i++) {
708 if (!parse_setdefinition(sets.elementAt(i))) {
713 /* parse relations */
714 for (int i = 0; i < relations.size(); i++) {
715 if (!parse_relationdefinition(relations.elementAt(i))) {
720 // ok, all the spaces have been parsed, now we should typecheck and check
723 // #TBD#: typecheck and check for cycles
725 /* replace missing with actual */
726 Iterator allsets = state.stSets.descriptors();
728 while (allsets.hasNext()) {
729 SetDescriptor sd = (SetDescriptor) allsets.next();
730 Vector subsets = sd.getSubsets();
732 for (int i = 0; i < subsets.size(); i++) {
733 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
735 if (subset instanceof MissingSetDescriptor) {
736 SetDescriptor newsubset = lookupSet(subset.getSymbol());
738 if (newsubset == null) {
739 er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
741 subsets.setElementAt(newsubset, i);
750 private boolean parse_setdefinition(ParseNode pn) {
751 if (!precheck(pn, "setdefinition")) {
758 String setname = pn.getChild("name").getTerminal();
759 assert (setname != null);
761 SetDescriptor sd = new SetDescriptor(setname);
764 String settype = pn.getChild("type").getTerminal();
765 TypeDescriptor type = lookupType(settype);
767 er.report(pn, "Undefined type '" + settype + "'");
773 /* is this a partition? */
774 boolean partition = pn.getChild("partition") != null;
775 sd.isPartition(partition);
777 /* if set has subsets, add them to set descriptor */
778 if (pn.getChild("setlist") != null) {
779 ParseNodeVector setlist = pn.getChild("setlist").getChildren();
781 for (int i = 0; i < setlist.size(); i++) {
782 String subsetname = setlist.elementAt(i).getLabel();
783 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
787 /* add set to symbol table */
788 if (stSets.contains(setname)) {
789 // Semantic Check: redefinition
790 er.report(pn, "Redefinition of set: " + setname);
799 private boolean parse_relationdefinition(ParseNode pn) {
800 if (!precheck(pn, "relationdefinition")) {
806 /* get relation name */
807 String relname = pn.getChild("name").getTerminal();
808 assert relname != null;
810 RelationDescriptor rd = new RelationDescriptor(relname);
812 /* check if static */
813 boolean bStatic = pn.getChild("static") != null;
814 rd.isStatic(bStatic);
817 String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
818 assert domainsetname != null;
821 String rangesetname = pn.getChild("range").getChild("type").getTerminal();
822 assert rangesetname != null;
824 /* get domain multiplicity */
826 if (pn.getChild("domain").getChild("domainmult") != null)
827 domainmult = pn.getChild("domain").getChild("domainmult").getChild("mult").getTerminal();
828 //assert domainmult != null;
830 /* get range multiplicity */
832 if (pn.getChild("range").getChild("domainrange") != null)
833 rangemult = pn.getChild("range").getChild("domainrange").getChild("mult").getTerminal();
834 //assert rangemult != null;
836 /* NOTE: it is assumed that the sets have been parsed already so that the
837 set namespace is fully populated. any missing setdescriptors for the set
838 symbol table will be assumed to be errors and reported. */
840 SetDescriptor domainset = lookupSet(domainsetname);
841 if (domainset == null) {
842 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
845 rd.setDomain(domainset);
848 SetDescriptor rangeset = lookupSet(rangesetname);
849 if (rangeset == null) {
850 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
853 rd.setRange(rangeset);
856 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
858 /* lets add the relation to the global symbol table */
859 if (!stRelations.contains(relname)) {
862 er.report(pn, "Redefinition of relation '" + relname + "'");
869 private boolean parse_structures(ParseNode pn) {
870 if (!precheck(pn, "structures")) {
875 ParseNodeVector structures = pn.getChildren("structure");
877 for (int i = 0; i < structures.size(); i++) {
878 if (!parse_structure(structures.elementAt(i))) {
883 ParseNodeVector globals = pn.getChildren("global");
885 for (int i = 0; i < globals.size(); i++) {
886 if (!parse_global(globals.elementAt(i))) {
891 // ok, all the structures have been parsed, now we gotta type check
893 Enumeration types = stTypes.getDescriptors();
894 while (types.hasMoreElements()) {
895 TypeDescriptor t = (TypeDescriptor) types.nextElement();
897 if (t instanceof ReservedTypeDescriptor) {
898 // we don't need to check reserved types
899 } else if (t instanceof StructureTypeDescriptor) {
901 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
902 TypeDescriptor subtype = type.getSuperType();
904 // check that the subtype is valid
905 if (subtype instanceof MissingTypeDescriptor) {
906 TypeDescriptor newtype = lookupType(subtype.getSymbol());
907 if (newtype == null) {
908 // subtype not defined anywheere
909 // #TBD#: somehow determine how we can get the original parsenode (global function?)
910 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
913 type.setSuperType(newtype);
917 Iterator fields = type.getFields();
919 while (fields.hasNext()) {
920 FieldDescriptor field = (FieldDescriptor) fields.next();
921 TypeDescriptor fieldtype = field.getType();
923 assert fieldtype != null;
925 // check that the type is valid
926 if (fieldtype instanceof MissingTypeDescriptor) {
927 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
928 if (newtype == null) {
929 // type never defined
930 // #TBD#: replace new ParseNode with original parsenode
932 if (!field.getPtr()) {
933 /* Pointer types don't have to be defined */
934 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
938 assert newtype != null;
939 field.setType(newtype);
944 Iterator labels = type.getLabels();
946 while (labels.hasNext()) {
947 LabelDescriptor label = (LabelDescriptor) labels.next();
948 TypeDescriptor labeltype = label.getType();
950 assert labeltype != null;
952 // check that the type is valid
953 if (labeltype instanceof MissingTypeDescriptor) {
954 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
955 if (newtype == null) {
956 // type never defined
957 // #TBD#: replace new ParseNode with original parsenode
958 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
961 assert newtype != null;
962 label.setType(newtype);
968 throw new IRException("shouldn't be any other typedescriptor classes");
976 types = stTypes.getDescriptors();
978 while (types.hasMoreElements()) {
979 TypeDescriptor t = (TypeDescriptor) types.nextElement();
981 if (t instanceof ReservedTypeDescriptor) {
982 // we don't need to check reserved types
983 } else if (t instanceof StructureTypeDescriptor) {
985 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
986 TypeDescriptor subtype = type.getSuperType();
987 Iterator fields = type.getFields();
989 while (fields.hasNext()) {
990 FieldDescriptor field = (FieldDescriptor) fields.next();
992 if (field instanceof ArrayDescriptor) {
993 ArrayDescriptor ad = (ArrayDescriptor) field;
994 Expr indexbound = ad.getIndexBound();
995 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
996 public IRErrorReporter getErrorReporter() { return er; }
997 public SymbolTable getSymbolTable() { return stGlobals; }
999 if (Compiler.REJECTLENGTH) {
1000 analyze_length(indexbound);
1004 if (indextype == null) {
1006 } else if (indextype != ReservedTypeDescriptor.INT) {
1007 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
1013 Iterator labels = type.getLabels();
1015 while (labels.hasNext()) {
1016 LabelDescriptor label = (LabelDescriptor) labels.next();
1017 Expr index = label.getIndex();
1019 if (index != null) {
1020 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
1021 public IRErrorReporter getErrorReporter() { return er; }
1022 public SymbolTable getSymbolTable() { return stGlobals; }
1025 if (indextype != ReservedTypeDescriptor.INT) {
1026 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
1032 throw new IRException("shouldn't be any other typedescriptor classes");
1036 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
1037 // subtypes, of course, are not real subtypes, they are merely a way to validate a
1043 private void analyze_length(Expr indexbound) {
1044 Set descriptors=indexbound.getRequiredDescriptors();
1045 for(Iterator it=descriptors.iterator();it.hasNext();) {
1046 Descriptor d=(Descriptor)it.next();
1047 if (d instanceof FieldDescriptor) {
1048 state.noupdate.add(d);
1049 } else if (d instanceof ArrayDescriptor) {
1050 state.noupdate.add(d);
1051 } else if (d instanceof VarDescriptor) {
1052 state.noupdate.add(d);
1057 private boolean parse_global(ParseNode pn) {
1058 if (!precheck(pn, "global")) {
1062 String name = pn.getChild("name").getTerminal();
1063 assert name != null;
1065 String type = pn.getChild("type").getTerminal();
1066 assert type != null;
1068 TypeDescriptor td = lookupType(type);
1071 if (stGlobals.contains(name)) {
1072 /* redefinition of global */
1073 er.report(pn, "Redefinition of global '" + name + "'");
1077 stGlobals.add(new VarDescriptor(name, name, td,true));
1081 private boolean parse_structure(ParseNode pn) {
1082 if (!precheck(pn, "structure")) {
1087 String typename = pn.getChild("name").getTerminal();
1088 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1090 if (pn.getChild("subtype") != null) {
1091 // has a subtype, lets try to resolve it
1092 String subtype = pn.getChild("subtype").getTerminal();
1094 if (subtype.equals(typename)) {
1095 // Semantic Error: cyclic inheritance
1096 er.report(pn, "Cyclic inheritance prohibited");
1100 /* lookup the type to get the type descriptor */
1101 type.setSuperType(lookupType(subtype, CREATE_MISSING));
1102 } else if (pn.getChild("subclass") != null) {
1103 // has a subtype, lets try to resolve it
1104 String subclass = pn.getChild("subclass").getTerminal();
1106 if (subclass.equals(typename)) {
1107 // Semantic Error: cyclic inheritance
1108 er.report(pn, "Cyclic inheritance prohibited");
1112 /* lookup the type to get the type descriptor */
1113 type.setSuperType(lookupType(subclass, CREATE_MISSING));
1114 type.setSubClass(true);
1117 // set the current type so that the recursive parses on the labels
1118 // and fields can add themselves automatically to the current type
1119 dCurrentType = type;
1121 // parse the labels and fields
1122 if (pn.getChild("lf")!=null && !parse_labelsandfields(pn.getChild("lf"))) {
1126 if (stTypes.contains(typename)) {
1127 er.report(pn, "Redefinition of type '" + typename + "'");
1136 private boolean parse_labelsandfields(ParseNode pn) {
1137 if (!precheck(pn, "lf")) {
1143 // check the fields first (need the field names
1144 // to type check the labels)
1145 if (!parse_fields(pn.getChild("fields"))) {
1149 // check the labels now that all the fields are sorted
1150 if (!parse_labels(pn.getChild("labels"))) {
1157 private boolean parse_fields(ParseNode pn) {
1158 if (!precheck(pn, "fields")) {
1164 /* NOTE: because the order of the fields is important when defining a data structure,
1165 and because the order is defined by the order of the fields defined in the field
1166 vector, its important that the parser returns the fields in the correct order */
1168 ParseNodeVector fields = pn.getChildren();
1170 for (int i = 0; i < fields.size(); i++) {
1171 ParseNode field = fields.elementAt(i);
1176 if (field.getChild("reserved") != null) {
1178 // #TBD#: it will be necessary for reserved field descriptors to generate
1179 // a unique symbol for the type descriptor requires it for its hashtable
1180 fd = new ReservedFieldDescriptor();
1183 name = field.getChild("name").getTerminal();
1184 fd = new FieldDescriptor(name);
1188 String type = field.getChild("type").getTerminal();
1189 boolean ptr = field.getChild("*") != null;
1192 fd.setType(lookupType(type, CREATE_MISSING));
1194 if (field.getChild("index") != null) {
1195 // field is an array, so create an array descriptor to wrap the
1196 // field descriptor and then replace the top level field descriptor with
1197 // this array descriptor
1198 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1200 // #ATTN#: do we really want to return an exception here?
1201 throw new IRException("invalid index expression");
1203 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1207 // add the current field to the current type
1208 if (reserved == false) {
1209 // lets double check that we are redefining a field
1210 if (dCurrentType.getField(name) != null) {
1211 // Semantic Error: field redefinition
1212 er.report(pn, "Redefinition of field '" + name + "'");
1215 dCurrentType.addField(fd);
1218 dCurrentType.addField(fd);
1225 private boolean parse_labels(ParseNode pn) {
1226 if (!precheck(pn, "labels")) {
1232 /* NOTE: parse_labels should be called after the fields have been parsed because any
1233 labels not found in the field set of the current type will be flagged as errors */
1235 ParseNodeVector labels = pn.getChildren();
1237 for (int i = 0; i < labels.size(); i++) {
1238 ParseNode label = labels.elementAt(i);
1239 String name = label.getChild("name").getTerminal();
1240 LabelDescriptor ld = new LabelDescriptor(name);
1242 if (label.getChild("index") != null) {
1243 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1245 /* #ATTN#: do we really want to return an exception here? */
1246 throw new IRException("Invalid expression");
1251 String type = label.getChild("type").getTerminal();
1253 ld.setType(lookupType(type, CREATE_MISSING));
1255 String field = label.getChild("field").getTerminal();
1256 FieldDescriptor fd = dCurrentType.getField(field);
1259 /* Semantic Error: Undefined field in label */
1260 er.report(label, "Undefined field '" + field + "' in label");
1266 /* add label to current type */
1267 if (dCurrentType.getLabel(name) != null) {
1268 /* semantic error: label redefinition */
1269 er.report(pn, "Redefinition of label '" + name + "'");
1272 dCurrentType.addLabel(ld);
1279 private Expr parse_expr(ParseNode pn) {
1280 if (!precheck(pn, "expr")) {
1284 if (pn.getChild("var") != null) {
1285 // we've got a variable reference... we'll have to scope check it later
1286 // when we are completely done... there are also some issues of cyclic definitions
1287 return new VarExpr(pn.getChild("var").getTerminal());
1288 } else if (pn.getChild("sumexpr") != null) {
1289 return parse_sum(pn.getChild("sumexpr"));
1290 } else if (pn.getChild("literal") != null) {
1291 return parse_literal(pn.getChild("literal"));
1292 } else if (pn.getChild("operator") != null) {
1293 return parse_operator(pn.getChild("operator"));
1294 } else if (pn.getChild("relation") != null) {
1295 return parse_relation(pn.getChild("relation"));
1296 } else if (pn.getChild("sizeof") != null) {
1297 return parse_sizeof(pn.getChild("sizeof"));
1298 } else if (pn.getChild("simple_expr") != null) {
1299 return parse_simple_expr(pn.getChild("simple_expr"));
1300 } else if (pn.getChild("elementof") != null) {
1301 return parse_elementof(pn.getChild("elementof"));
1302 } else if (pn.getChild("tupleof") != null) {
1303 return parse_tupleof(pn.getChild("tupleof"));
1304 } else if (pn.getChild("isvalid") != null) {
1305 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1308 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1313 private Expr parse_elementof(ParseNode pn) {
1314 if (!precheck(pn, "elementof")) {
1319 String setname = pn.getChild("name").getTerminal();
1320 assert setname != null;
1321 SetDescriptor sd = lookupSet(setname);
1324 er.report(pn, "Undefined set '" + setname + "'");
1328 /* get left side expr */
1329 Expr expr = parse_expr(pn.getChild("expr"));
1335 return new ElementOfExpr(expr, sd);
1338 private Expr parse_tupleof(ParseNode pn) {
1339 if (!precheck(pn, "tupleof")) {
1344 String relname = pn.getChild("name").getTerminal();
1345 assert relname != null;
1346 RelationDescriptor rd = lookupRelation(relname);
1349 er.report(pn, "Undefined relation '" + relname + "'");
1353 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1354 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1356 if ((left == null) || (right == null)) {
1360 return new TupleOfExpr(left, right, rd);
1363 private Expr parse_simple_expr(ParseNode pn) {
1364 if (!precheck(pn, "simple_expr")) {
1368 // only locations so far
1369 return parse_location(pn.getChild("location"));
1372 private Expr parse_location(ParseNode pn) {
1373 if (!precheck(pn, "location")) {
1377 if (pn.getChild("var") != null) {
1378 // should be changed into a namespace check */
1379 return new VarExpr(pn.getChild("var").getTerminal());
1380 } else if (pn.getChild("cast") != null) {
1381 return parse_cast(pn.getChild("cast"));
1382 } else if (pn.getChild("dot") != null) {
1383 return parse_dot(pn.getChild("dot"));
1385 throw new IRException();
1389 private RelationExpr parse_relation(ParseNode pn) {
1390 if (!precheck(pn, "relation")) {
1394 String relname = pn.getChild("name").getTerminal();
1395 boolean inverse = pn.getChild("inv") != null;
1396 Expr expr = parse_expr(pn.getChild("expr"));
1402 RelationDescriptor relation = lookupRelation(relname);
1404 if (relation == null) {
1405 /* Semantic Error: relation not definied" */
1406 er.report(pn, "Undefined relation '" + relname + "'");
1410 /* add usage so correct sets are created */
1411 relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
1413 return new RelationExpr(expr, relation, inverse);
1416 private SizeofExpr parse_sizeof(ParseNode pn) {
1417 if (!precheck(pn, "sizeof")) {
1422 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1424 if (setexpr == null) {
1428 return new SizeofExpr(setexpr);
1431 private SumExpr parse_sum(ParseNode pn) {
1432 if (!precheck(pn, "sumexpr")) {
1435 String setname = pn.getChild("dot").getChild("set").getTerminal();
1436 assert setname != null;
1437 SetDescriptor sd = lookupSet(setname);
1440 er.report(pn, "Unknown or undefined set '" + setname + "'");
1444 RelationDescriptor rd = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1445 rd.addUsage(RelationDescriptor.IMAGE);
1447 return new SumExpr(sd,rd);
1450 private CastExpr parse_cast(ParseNode pn) {
1451 if (!precheck(pn, "cast")) {
1456 String typename = pn.getChild("type").getTerminal();
1457 assert typename != null;
1458 TypeDescriptor type = lookupType(typename);
1461 /* semantic error: undefined type in cast */
1462 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1467 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1473 return new CastExpr(type, expr);
1476 private SetExpr parse_setexpr(ParseNode pn) {
1477 if (!precheck(pn, "setexpr")) {
1481 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1483 if (pn.getChild("set") != null) {
1484 String setname = pn.getChild("set").getTerminal();
1485 assert setname != null;
1486 SetDescriptor sd = lookupSet(setname);
1489 er.report(pn, "Unknown or undefined set '" + setname + "'");
1492 return new SetExpr(sd);
1494 } else if (pn.getChild("dot") != null) {
1495 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1496 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1497 relation.addUsage(RelationDescriptor.IMAGE);
1498 return new ImageSetExpr(vd, relation);
1499 } else if (pn.getChild("dotinv") != null) {
1500 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1501 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1502 relation.addUsage(RelationDescriptor.INVIMAGE);
1503 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1504 } else if (pn.getChild("dotset") != null) {
1505 ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotset").getChild("setexpr"));
1506 RelationDescriptor relation = lookupRelation(pn.getChild("dotset").getChild("relation").getTerminal());
1507 relation.addUsage(RelationDescriptor.IMAGE);
1508 return new ImageSetExpr(ise, relation);
1509 } else if (pn.getChild("dotinvset") != null) {
1510 ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotinvset").getChild("setexpr"));
1511 RelationDescriptor relation = lookupRelation(pn.getChild("dotinvset").getChild("relation").getTerminal());
1512 relation.addUsage(RelationDescriptor.INVIMAGE);
1513 return new ImageSetExpr(ImageSetExpr.INVERSE, ise, relation);
1515 throw new IRException();
1519 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1520 if (!precheck(pn, "quantifiervar")) {
1525 String varname = pn.getTerminal();
1526 assert varname != null;
1528 /* NOTE: quantifier var's are only found in the constraints and
1529 model definitions... therefore we can do a semantic check here
1530 to make sure that the variables exist in the symbol table */
1532 /* NOTE: its assumed that the symbol table stack is appropriately
1533 set up with the parent quantifier symbol table */
1534 assert !sts.empty();
1536 /* do semantic check and if valid, add it to symbol table
1537 and add it to the quantifier as well */
1538 if (sts.peek().contains(varname)) {
1539 VarDescriptor vdold=(VarDescriptor)sts.peek().get(varname);
1541 /* Dan was creating a new VarDescriptor...This seems
1542 like the wrong thing to do. We'll just lookup the
1544 --------------------------------------------------
1545 VarDescriptor vd=new VarDescriptor(varname);
1546 vd.setSet(vdold.getSet()); return vd;*/
1548 /* Semantic Error: undefined variable */
1549 er.report(pn, "Undefined variable '" + varname + "'");
1554 private LiteralExpr parse_literal(ParseNode pn) {
1555 if (!precheck(pn, "literal")) {
1559 if (pn.getChild("boolean") != null) {
1560 if (pn.getChild("boolean").getChild("true") != null) {
1561 return new BooleanLiteralExpr(true);
1563 return new BooleanLiteralExpr(false);
1565 } else if (pn.getChild("decimal") != null) {
1566 String integer = pn.getChild("decimal").getTerminal();
1568 /* Check for integer literal overflow */
1569 BigInteger intLitBI = new BigInteger(integer);
1570 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1571 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1574 if (intLitBI.compareTo(intMin) < 0) {
1575 value = Integer.MIN_VALUE;
1576 er.warn(pn, "Integer literal overflow");
1577 } else if (intLitBI.compareTo(intMax) > 0) {
1578 value = Integer.MAX_VALUE;
1579 er.warn(pn, "Integer literal overflow");
1581 /* no truncation needed */
1582 value = Integer.parseInt(integer);
1585 return new IntegerLiteralExpr(value);
1586 } else if (pn.getChild("token") != null) {
1587 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1588 } else if (pn.getChild("string") != null) {
1589 throw new IRException("string unsupported");
1590 } else if (pn.getChild("char") != null) {
1591 throw new IRException("char unsupported");
1593 throw new IRException("unknown literal expression type.");
1597 private OpExpr parse_operator(ParseNode pn) {
1598 if (!precheck(pn, "operator")) {
1602 String opname = pn.getChild("op").getTerminal();
1603 Opcode opcode = Opcode.decodeFromString(opname);
1605 if (opcode == null) {
1606 er.report(pn, "Unsupported operation: " + opname);
1610 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1613 if (pn.getChild("right") != null) {
1614 right = parse_expr(pn.getChild("right").getChild("expr"));
1621 if (right == null && opcode != Opcode.NOT) {
1622 er.report(pn, "Two arguments required.");
1626 return new OpExpr(opcode, left, right);
1629 private DotExpr parse_dot(ParseNode pn) {
1630 if (!precheck(pn, "dot")) {
1634 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1640 String field = pn.getChild("field").getTerminal();
1644 if (pn.getChild("index") != null) {
1645 index = parse_expr(pn.getChild("index").getChild("expr"));
1647 if (index == null) {
1652 return new DotExpr(left, field, index);