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;
38 // Don't clear the state!! Do clear the IR-related state
39 this.state.stTypes = null;
42 throw new IRException("IRBuilder.build: Received null ErrorReporter");
47 if (state.ptStructures == null) {
48 throw new IRException("IRBuilder.build: Received null ParseNode");
51 state.vConstraints = new Vector();
52 vConstraints = state.vConstraints;
54 state.vRules = new Vector();
55 vRules = state.vRules;
57 state.stTypes = new SymbolTable();
58 stTypes = state.stTypes;
60 state.stSets = new SymbolTable();
61 stSets = state.stSets;
63 state.stRelations = new SymbolTable();
64 stRelations = state.stRelations;
66 state.stGlobals = new SymbolTable();
67 stGlobals = state.stGlobals;
69 sts = new SymbolTableStack();
71 // add int and bool to the types list
72 stTypes.add(ReservedTypeDescriptor.BIT);
73 stTypes.add(ReservedTypeDescriptor.BYTE);
74 stTypes.add(ReservedTypeDescriptor.SHORT);
75 stTypes.add(ReservedTypeDescriptor.INT);
77 stSets.add(new ReservedSetDescriptor("int", ReservedTypeDescriptor.INT));
78 stSets.add(new ReservedSetDescriptor("token", ReservedTypeDescriptor.INT));
82 er.setFilename(state.infile + ".struct");
83 if (!parse_structures(state.ptStructures)) {
87 er.setFilename(state.infile + ".space");
88 if (!parse_space(state.ptSpace)) {
92 er.setFilename(state.infile + ".constraints");
93 if (!parse_constraints(state.ptConstraints)) {
97 er.setFilename(state.infile + ".model");
98 if (!parse_rules(state.ptModel)) {
105 /********************** HELPER FUNCTIONS ************************/
108 * special case lookup that returns null if no such type exists
110 private TypeDescriptor lookupType(String typename) {
111 return lookupType(typename, false);
115 * does a look up in the types symbol table. if the type is
116 * not found than a missing type descriptor is returned
118 private TypeDescriptor lookupType(String typename, boolean createmissing) {
119 if (stTypes.get(typename) != null) {
120 // the type exists, so plug in the descriptor directly
121 return (TypeDescriptor) stTypes.get(typename);
122 } else if (createmissing) {
123 return new MissingTypeDescriptor(typename);
132 private VarDescriptor reserveName(ParseNode pn) {
134 String varname = pn.getTerminal();
135 assert varname != null;
137 /* do semantic check and if valid, add it to symbol table
138 and add it to the quantifier as well */
139 if (sts.peek().contains(varname)) {
140 /* Semantic Error: redefinition */
141 er.report(pn, "Redefinition of '" + varname + "'");
144 VarDescriptor vd = new VarDescriptor(varname);
151 * special case lookup that returns null if no such set exists
153 private SetDescriptor lookupSet(String setname) {
154 return lookupSet(setname, false);
158 * does a look up in the set's symbol table. if the set is
159 * not found than a missing set descriptor is returned
161 private SetDescriptor lookupSet(String setname, boolean createmissing) {
162 if (stSets.get(setname) != null) {
163 // the set exists, so plug in the descriptor directly
164 return (SetDescriptor) stSets.get(setname);
165 } else if (createmissing) {
166 return new MissingSetDescriptor(setname);
173 * does a look up in the set's symbol table. if the set is
174 * not found than a missing set descriptor is returned
176 private RelationDescriptor lookupRelation(String relname) {
177 if (stRelations.get(relname) != null) {
178 // the relation exists, so plug in the descriptor directly
179 return (RelationDescriptor) stRelations.get(relname);
186 private static int count = 0;
187 private boolean precheck(ParseNode pn, String label) {
189 er.report(pn, "IE: Expected '" + label + "', got null");
194 if (! pn.getLabel().equals(label)) {
195 er.report(pn, "IE: Expected '" + label + "', got '" + pn.getLabel() + "'");
200 if (state.verbose >= 2) {
201 System.err.println("visiting*" + (count++) + ": " + label);
207 /********************* PARSING FUNCTIONS ************************/
209 private boolean parse_rules(ParseNode pn) {
210 if (!precheck(pn, "rules")) {
215 ParseNodeVector rules = pn.getChildren();
217 for (int i = 0; i < rules.size(); i++) {
218 ParseNode rule = rules.elementAt(i);
219 if (!parse_rule(rule)) {
225 Iterator ruleiterator = state.vRules.iterator();
227 while (ruleiterator.hasNext()) {
228 Rule rule = (Rule) ruleiterator.next();
229 Expr guard = rule.getGuardExpr();
230 final SymbolTable rulest = rule.getSymbolTable();
231 SemanticAnalyzer sa = new SemanticAnalyzer() {
232 public IRErrorReporter getErrorReporter() { return er; }
233 public SymbolTable getSymbolTable() { return rulest; }
235 TypeDescriptor guardtype = guard.typecheck(sa);
237 if (guardtype == null) {
239 } else if (guardtype != ReservedTypeDescriptor.INT) {
240 er.report(null, "Type of guard must be 'int' not '" + guardtype.getSymbol() + "'");
244 if (!rule.getInclusion().typecheck(sa)) {
248 Iterator quantifiers = rule.quantifiers();
250 while (quantifiers.hasNext()) {
251 Quantifier q = (Quantifier) quantifiers.next();
253 if (q instanceof ForQuantifier && !((ForQuantifier)q).typecheck(sa)) {
259 /* do any post checks ?? */
264 private boolean parse_rule(ParseNode pn) {
265 if (!precheck(pn, "rule")) {
270 Rule rule = new Rule();
273 boolean isstatic = pn.getChild("static") != null;
274 boolean isdelay = pn.getChild("delay") != null;
275 rule.setStatic(isstatic);
276 rule.setDelay(isdelay);
278 /* set up symbol table for constraint */
281 sts.push(rule.getSymbolTable());
283 /* optional quantifiers */
284 if (pn.getChild("quantifiers") != null) {
285 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
287 for (int i = 0; i < quantifiers.size(); i++) {
288 ParseNode qn = quantifiers.elementAt(i);
289 Quantifier quantifier = parse_quantifier(qn);
291 if (quantifier == null) {
294 rule.addQuantifier(quantifier);
300 Expr guard = parse_expr(pn.getChild("expr"));
305 rule.setGuardExpr(guard);
308 /* inclusion constraint */
309 Inclusion inclusion = parse_inclusion(pn.getChild("inclusion"));
311 if (inclusion == null) {
314 rule.setInclusion(inclusion);
317 /* pop symbol table stack */
318 SymbolTable st = sts.pop();
319 sts.pop(); /* pop off globals */
321 /* make sure the stack we pop is our rule s.t. */
322 assert st == rule.getSymbolTable();
325 /* add rule to global set */
326 vRules.addElement(rule);
331 private Inclusion parse_inclusion(ParseNode pn) {
332 if (!precheck(pn, "inclusion")) {
336 if (pn.getChild("set") != null) {
337 ParseNode set = pn.getChild("set");
338 Expr expr = parse_expr(set.getChild("expr"));
344 String setname = set.getChild("name").getTerminal();
345 assert setname != null;
346 SetDescriptor sd = lookupSet(setname);
349 er.report(set.getChild("name"), "Undefined set '" + setname + "'");
353 return new SetInclusion(expr, sd);
354 } else if (pn.getChild("relation") != null) {
355 ParseNode relation = pn.getChild("relation");
356 Expr leftexpr = parse_expr(relation.getChild("left").getChild("expr"));
357 Expr rightexpr = parse_expr(relation.getChild("right").getChild("expr"));
359 if ((leftexpr == null) || (rightexpr == null)) {
363 String relname = relation.getChild("name").getTerminal();
364 assert relname != null;
365 RelationDescriptor rd = lookupRelation(relname);
368 er.report(relation.getChild("name"), "Undefined relation '" + relname + "'");
372 return new RelationInclusion(leftexpr, rightexpr, rd);
374 throw new IRException();
378 private boolean parse_constraints(ParseNode pn) {
379 if (!precheck(pn, "constraints")) {
384 ParseNodeVector constraints = pn.getChildren();
386 for (int i = 0; i < constraints.size(); i++) {
387 ParseNode constraint = constraints.elementAt(i);
388 assert constraint.getLabel().equals("constraint");
389 if (!parse_constraint(constraint)) {
394 /* do any post checks... (type constraints, etc?) */
399 private boolean parse_constraint(ParseNode pn) {
400 if (!precheck(pn, "constraint")) {
405 Constraint constraint = new Constraint();
408 boolean crash = pn.getChild("crash") != null;
409 constraint.setCrash(crash);
411 /* set up symbol table for constraint */
413 sts.push(constraint.getSymbolTable());
415 /* get quantifiers */
416 if (pn.getChild("quantifiers") != null) {
417 ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
419 for (int i = 0; i < quantifiers.size(); i++) {
420 ParseNode qn = quantifiers.elementAt(i);
421 assert qn.getLabel().equals("quantifier");
422 Quantifier quantifier = parse_quantifier(qn);
423 if (quantifier == null) {
426 constraint.addQuantifier(quantifier);
432 LogicStatement logicexpr = parse_body(pn.getChild("body"));
434 if (logicexpr == null) {
437 constraint.setLogicStatement(logicexpr);
440 /* pop symbol table stack */
441 SymbolTable st = sts.pop();
443 /* make sure the stack we pop is our constraint s.t. */
444 assert st == constraint.getSymbolTable();
447 /* add to vConstraints */
448 vConstraints.addElement(constraint);
453 private Quantifier parse_quantifier(ParseNode pn) {
454 if (!precheck(pn, "quantifier")) {
458 if (pn.getChild("forall") != null) { /* forall element in Set */
459 SetQuantifier sq = new SetQuantifier();
462 VarDescriptor vd = reserveName(pn.getChild("var"));
471 SetDescriptor set = parse_set(pn.getChild("set"));
475 vd.setType(set.getType());
477 /* return to caller */
480 } else if (pn.getChild("relatiion") != null) { /* for < v1, v2 > in Relation */
481 RelationQuantifier rq = new RelationQuantifier();
484 VarDescriptor vd1 = reserveName(pn.getChild("left"));
485 VarDescriptor vd2 = reserveName(pn.getChild("right"));
487 if ((vd1 == null) || (vd2 == null)) {
491 rq.setTuple(vd1, vd2);
494 String relationname = pn.getChild("relation").getTerminal();
495 assert relationname != null;
496 RelationDescriptor rd = lookupRelation(relationname);
503 vd1.setType(rd.getDomain().getType());
504 vd2.setType(rd.getRange().getType());
506 } else if (pn.getChild("for") != null) { /* for j = x to y */
507 ForQuantifier fq = new ForQuantifier();
510 VarDescriptor vd = reserveName(pn.getChild("var"));
516 vd.setType(ReservedTypeDescriptor.INT);
519 /* grab lower/upper bounds */
520 Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
521 Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
523 if ((lower == null) || (upper == null)) {
527 fq.setBounds(lower, upper);
531 throw new IRException("not supported yet");
536 private LogicStatement parse_body(ParseNode pn) {
537 if (!precheck(pn, "body")) {
541 if (pn.getChild("and") != null) {
543 LogicStatement left, right;
544 left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
545 right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
547 if ((left == null) || (right == null)) {
551 // what do we want to call the and/or/not body classes?
552 return new LogicStatement(LogicStatement.AND, left, right);
553 } else if (pn.getChild("or") != null) {
555 LogicStatement left, right;
556 left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
557 right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
559 if ((left == null) || (right == null)) {
563 return new LogicStatement(LogicStatement.OR, left, right);
564 } else if (pn.getChild("not") != null) {
566 LogicStatement left = parse_body(pn.getChild("not").getChild("left").getChild("body"));
572 return new LogicStatement(LogicStatement.NOT, left);
573 } else if (pn.getChild("predicate") != null) {
574 return parse_predicate(pn.getChild("predicate"));
576 throw new IRException();
580 private Predicate parse_predicate(ParseNode pn) {
581 if (!precheck(pn, "predicate")) {
585 if (pn.getChild("inclusion") != null) {
586 ParseNode in = pn.getChild("inclusion");
588 /* get quantiifer var */
589 VarDescriptor vd = parse_quantifiervar(in.getChild("quantifiervar"));
596 SetExpr setexpr = parse_setexpr(in.getChild("setexpr"));
598 if (setexpr == null) {
602 return new InclusionPredicate(vd, setexpr);
603 } else if (pn.getChild("sizeof") != null) {
604 ParseNode sizeof = pn.getChild("sizeof");
607 SetExpr setexpr = parse_setexpr(sizeof.getChild("setexpr"));
609 if (setexpr == null) {
613 /* get comparison operator */
614 String compareop = sizeof.getChild("compare").getTerminal();
615 Opcode opcode = Opcode.decodeFromString(opname);
617 if (opcode == null) {
618 er.report(pn, "Unsupported operation: " + opname);
624 return new InclusionPredicate(vd, setexpr);
625 } else if (pn.getChild("comparison") != null) {
626 ParseNode cn = pn.getChild("comparison");
629 Expr left = parse_expr(cn.getChild("left").getChild("expr"));
630 Expr right = parse_expr(cn.getChild("right").getChild("expr"));
632 if ((left == null) || (right == null)) {
636 /* get comparison operator */
637 String comparison = cn.getChild("compare").getTerminal();
638 assert comparison != null;
640 return new ComparisonPredicate(comparison, left, right);
642 throw new IRException();
646 private SetDescriptor parse_set(ParseNode pn) {
647 if (!precheck(pn, "set")) {
651 if (pn.getChild("name") != null) {
652 String setname = pn.getChild("name").getTerminal();
653 assert setname != null;
655 if (!stSets.contains(setname)) {
656 /* Semantic Error: unknown set */
657 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
660 /* all good, get setdescriptor */
661 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
665 } else if (pn.getChild("listofliterals") != null) {
666 TokenSetDescriptor tokenset = new TokenSetDescriptor();
667 ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
668 assert token_literals.size() > 0;
670 for (int i = 0; i < token_literals.size(); i++) {
671 ParseNode literal = token_literals.elementAt(i);
672 assert literal.getLabel().equals("literal");
673 LiteralExpr litexpr = parse_literal(literal);
675 if (litexpr == null) {
679 if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
680 tokenset.addLiteral(litexpr);
682 er.report(literal, "Elements of a user-defined set must be of type token or integer");
683 // return null; /* don't think we need to return null */
689 throw new IRException(pn.getTerminal());
693 private boolean parse_space(ParseNode pn) {
694 if (!precheck(pn, "space")) {
699 ParseNodeVector sets = pn.getChildren("setdefinition");
700 ParseNodeVector relations = pn.getChildren("relationdefinition");
702 assert pn.getChildren().size() == (sets.size() + relations.size());
705 for (int i = 0; i < sets.size(); i++) {
706 if (!parse_setdefinition(sets.elementAt(i))) {
711 /* parse relations */
712 for (int i = 0; i < relations.size(); i++) {
713 if (!parse_relationdefinition(relations.elementAt(i))) {
718 // ok, all the spaces have been parsed, now we should typecheck and check
721 // #TBD#: typecheck and check for cycles
723 /* replace missing with actual */
724 Iterator allsets = state.stSets.descriptors();
726 while (allsets.hasNext()) {
727 SetDescriptor sd = (SetDescriptor) allsets.next();
728 Vector subsets = sd.getSubsets();
730 for (int i = 0; i < subsets.size(); i++) {
731 SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
733 if (subset instanceof MissingSetDescriptor) {
734 SetDescriptor newsubset = lookupSet(subset.getSymbol());
736 if (newsubset == null) {
737 er.report(null, "Unknown subset '" + subset.getSymbol() + "'");
739 subsets.setElementAt(newsubset, i);
748 private boolean parse_setdefinition(ParseNode pn) {
749 if (!precheck(pn, "setdefinition")) {
756 String setname = pn.getChild("name").getTerminal();
757 assert (setname != null);
759 SetDescriptor sd = new SetDescriptor(setname);
762 String settype = pn.getChild("type").getTerminal();
763 TypeDescriptor type = lookupType(settype);
765 er.report(pn, "Undefined type '" + settype + "'");
771 /* is this a partition? */
772 boolean partition = pn.getChild("partition") != null;
773 sd.isPartition(partition);
775 /* if set has subsets, add them to set descriptor */
776 if (pn.getChild("setlist") != null) {
777 ParseNodeVector setlist = pn.getChild("setlist").getChildren();
779 for (int i = 0; i < setlist.size(); i++) {
780 String subsetname = setlist.elementAt(i).getLabel();
781 sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
785 /* add set to symbol table */
786 if (stSets.contains(setname)) {
787 // Semantic Check: redefinition
788 er.report(pn, "Redefinition of set: " + setname);
797 private boolean parse_relationdefinition(ParseNode pn) {
798 if (!precheck(pn, "relationdefinition")) {
804 /* get relation name */
805 String relname = pn.getChild("name").getTerminal();
806 assert relname != null;
808 RelationDescriptor rd = new RelationDescriptor(relname);
810 /* check if static */
811 boolean bStatic = pn.getChild("static") != null;
812 rd.isStatic(bStatic);
815 String domainsetname = pn.getChild("domain").getChild("type").getTerminal();
816 assert domainsetname != null;
819 String rangesetname = pn.getChild("range").getChild("type").getTerminal();
820 assert rangesetname != null;
822 /* get domain multiplicity */
823 String domainmult = pn.getChild("domain").getChild("mult").getTerminal();
824 assert domainmult != null;
826 /* get range multiplicity */
827 String rangemult = pn.getChild("range").getChild("mult").getTerminal();
828 assert rangemult != null;
830 /* NOTE: it is assumed that the sets have been parsed already so that the
831 set namespace is fully populated. any missing setdescriptors for the set
832 symbol table will be assumed to be errors and reported. */
834 SetDescriptor domainset = lookupSet(domainsetname);
835 if (domainset == null) {
836 er.report(pn, "Undefined set '" + domainsetname + "' referenced in relation '" + relname + "'");
839 rd.setDomain(domainset);
842 SetDescriptor rangeset = lookupSet(rangesetname);
843 if (rangeset == null) {
844 er.report(pn, "Undefined set '" + rangesetname + "' referenced in relation '" + relname + "'");
847 rd.setRange(rangeset);
850 // #TBD#: eventually we'll use the multiplicities but now we don't... oh well
852 /* lets add the relation to the global symbol table */
853 if (!stRelations.contains(relname)) {
856 er.report(pn, "Redefinition of relation '" + relname + "'");
863 private boolean parse_structures(ParseNode pn) {
864 if (!precheck(pn, "structures")) {
869 ParseNodeVector structures = pn.getChildren("structure");
871 for (int i = 0; i < structures.size(); i++) {
872 if (!parse_structure(structures.elementAt(i))) {
877 ParseNodeVector globals = pn.getChildren("global");
879 for (int i = 0; i < globals.size(); i++) {
880 if (!parse_global(globals.elementAt(i))) {
885 // ok, all the structures have been parsed, now we gotta type check
887 Enumeration types = stTypes.getDescriptors();
888 while (types.hasMoreElements()) {
889 TypeDescriptor t = (TypeDescriptor) types.nextElement();
891 if (t instanceof ReservedTypeDescriptor) {
892 // we don't need to check reserved types
893 } else if (t instanceof StructureTypeDescriptor) {
895 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
896 TypeDescriptor subtype = type.getSubType();
898 // check that the subtype is valid
899 if (subtype instanceof MissingTypeDescriptor) {
900 TypeDescriptor newtype = lookupType(subtype.getSymbol());
901 if (newtype == null) {
902 // subtype not defined anywheere
903 // #TBD#: somehow determine how we can get the original parsenode (global function?)
904 er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
907 type.setSubType(newtype);
911 Iterator fields = type.getFields();
913 while (fields.hasNext()) {
914 FieldDescriptor field = (FieldDescriptor) fields.next();
915 TypeDescriptor fieldtype = field.getType();
917 assert fieldtype != null;
919 // check that the type is valid
920 if (fieldtype instanceof MissingTypeDescriptor) {
921 TypeDescriptor newtype = lookupType(fieldtype.getSymbol());
922 if (newtype == null) {
923 // type never defined
924 // #TBD#: replace new ParseNode with original parsenode
925 er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
928 assert newtype != null;
929 field.setType(newtype);
934 Iterator labels = type.getLabels();
936 while (labels.hasNext()) {
937 LabelDescriptor label = (LabelDescriptor) labels.next();
938 TypeDescriptor labeltype = label.getType();
940 assert labeltype != null;
942 // check that the type is valid
943 if (labeltype instanceof MissingTypeDescriptor) {
944 TypeDescriptor newtype = lookupType(labeltype.getSymbol());
945 if (newtype == null) {
946 // type never defined
947 // #TBD#: replace new ParseNode with original parsenode
948 er.report(null, "Undefined type '" + labeltype.getSymbol() + "'");
951 assert newtype != null;
952 label.setType(newtype);
958 throw new IRException("shouldn't be any other typedescriptor classes");
966 types = stTypes.getDescriptors();
968 while (types.hasMoreElements()) {
969 TypeDescriptor t = (TypeDescriptor) types.nextElement();
971 if (t instanceof ReservedTypeDescriptor) {
972 // we don't need to check reserved types
973 } else if (t instanceof StructureTypeDescriptor) {
975 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
976 TypeDescriptor subtype = type.getSubType();
977 Iterator fields = type.getFields();
979 while (fields.hasNext()) {
980 FieldDescriptor field = (FieldDescriptor) fields.next();
982 if (field instanceof ArrayDescriptor) {
983 ArrayDescriptor ad = (ArrayDescriptor) field;
984 Expr indexbound = ad.getIndexBound();
985 TypeDescriptor indextype = indexbound.typecheck(new SemanticAnalyzer() {
986 public IRErrorReporter getErrorReporter() { return er; }
987 public SymbolTable getSymbolTable() { return stGlobals; }
990 if (indextype == null) {
992 } else if (indextype != ReservedTypeDescriptor.INT) {
993 er.report(null, "'" + type.getSymbol() + "." + field.getSymbol() + "' index bounds must be type 'int' not '" + indextype.getSymbol() + "'");
999 Iterator labels = type.getLabels();
1001 while (labels.hasNext()) {
1002 LabelDescriptor label = (LabelDescriptor) labels.next();
1003 Expr index = label.getIndex();
1005 if (index != null) {
1006 TypeDescriptor indextype = index.typecheck(new SemanticAnalyzer() {
1007 public IRErrorReporter getErrorReporter() { return er; }
1008 public SymbolTable getSymbolTable() { return stGlobals; }
1011 if (indextype != ReservedTypeDescriptor.INT) {
1012 er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
1019 throw new IRException("shouldn't be any other typedescriptor classes");
1024 // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
1025 // subtypes, of course, are not real subtypes, they are merely a way to validate a
1031 private boolean parse_global(ParseNode pn) {
1032 if (!precheck(pn, "global")) {
1036 String name = pn.getChild("name").getTerminal();
1037 assert name != null;
1039 String type = pn.getChild("type").getTerminal();
1040 assert type != null;
1041 TypeDescriptor td = lookupType(type);
1043 assert !(td instanceof ReservedTypeDescriptor);
1045 if (stGlobals.contains(name)) {
1046 /* redefinition of global */
1047 er.report(pn, "Redefinition of global '" + name + "'");
1051 stGlobals.add(new VarDescriptor(name, name, td));
1055 private boolean parse_structure(ParseNode pn) {
1056 if (!precheck(pn, "structure")) {
1061 String typename = pn.getChild("name").getTerminal();
1062 StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
1064 if (pn.getChild("subtype") != null) {
1065 // has a subtype, lets try to resolve it
1066 String subtype = pn.getChild("subtype").getTerminal();
1068 if (subtype.equals(typename)) {
1069 // Semantic Error: cyclic inheritance
1070 er.report(pn, "Cyclic inheritance prohibited");
1074 /* lookup the type to get the type descriptor */
1075 type.setSubType(lookupType(subtype, CREATE_MISSING));
1078 // set the current type so that the recursive parses on the labels
1079 // and fields can add themselves automatically to the current type
1080 dCurrentType = type;
1082 // parse the labels and fields
1083 if (!parse_labelsandfields(pn.getChild("lf"))) {
1087 if (stTypes.contains(typename)) {
1088 er.report(pn, "Redefinition of type '" + typename + "'");
1097 private boolean parse_labelsandfields(ParseNode pn) {
1098 if (!precheck(pn, "lf")) {
1104 // check the fields first (need the field names
1105 // to type check the labels)
1106 if (!parse_fields(pn.getChild("fields"))) {
1110 // check the labels now that all the fields are sorted
1111 if (!parse_labels(pn.getChild("labels"))) {
1118 private boolean parse_fields(ParseNode pn) {
1119 if (!precheck(pn, "fields")) {
1125 /* NOTE: because the order of the fields is important when defining a data structure,
1126 and because the order is defined by the order of the fields defined in the field
1127 vector, its important that the parser returns the fields in the correct order */
1129 ParseNodeVector fields = pn.getChildren();
1131 for (int i = 0; i < fields.size(); i++) {
1132 ParseNode field = fields.elementAt(i);
1137 if (field.getChild("reserved") != null) {
1139 // #TBD#: it will be necessary for reserved field descriptors to generate
1140 // a unique symbol for the type descriptor requires it for its hashtable
1141 fd = new ReservedFieldDescriptor();
1144 name = field.getChild("name").getTerminal();
1145 fd = new FieldDescriptor(name);
1149 String type = field.getChild("type").getTerminal();
1150 boolean ptr = field.getChild("*") != null;
1153 fd.setType(lookupType(type, CREATE_MISSING));
1155 if (field.getChild("index") != null) {
1156 // field is an array, so create an array descriptor to wrap the
1157 // field descriptor and then replace the top level field descriptor with
1158 // this array descriptor
1159 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
1161 // #ATTN#: do we really want to return an exception here?
1162 throw new IRException("invalid index expression");
1164 ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
1168 // add the current field to the current type
1169 if (reserved == false) {
1170 // lets double check that we are redefining a field
1171 if (dCurrentType.getField(name) != null) {
1172 // Semantic Error: field redefinition
1173 er.report(pn, "Redefinition of field '" + name + "'");
1176 dCurrentType.addField(fd);
1179 dCurrentType.addField(fd);
1186 private boolean parse_labels(ParseNode pn) {
1187 if (!precheck(pn, "labels")) {
1193 /* NOTE: parse_labels should be called after the fields have been parsed because any
1194 labels not found in the field set of the current type will be flagged as errors */
1196 ParseNodeVector labels = pn.getChildren();
1198 for (int i = 0; i < labels.size(); i++) {
1199 ParseNode label = labels.elementAt(i);
1200 String name = label.getChild("name").getTerminal();
1201 LabelDescriptor ld = new LabelDescriptor(name);
1203 if (label.getChild("index") != null) {
1204 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
1206 /* #ATTN#: do we really want to return an exception here? */
1207 throw new IRException("Invalid expression");
1212 String type = label.getChild("type").getTerminal();
1214 ld.setType(lookupType(type, CREATE_MISSING));
1216 String field = label.getChild("field").getTerminal();
1217 FieldDescriptor fd = dCurrentType.getField(field);
1220 /* Semantic Error: Undefined field in label */
1221 er.report(label, "Undefined field '" + field + "' in label");
1227 /* add label to current type */
1228 if (dCurrentType.getLabel(name) != null) {
1229 /* semantic error: label redefinition */
1230 er.report(pn, "Redefinition of label '" + name + "'");
1233 dCurrentType.addLabel(ld);
1240 private Expr parse_expr(ParseNode pn) {
1241 if (!precheck(pn, "expr")) {
1245 if (pn.getChild("var") != null) {
1246 // we've got a variable reference... we'll have to scope check it later
1247 // when we are completely done... there are also some issues of cyclic definitions
1248 return new VarExpr(pn.getChild("var").getTerminal());
1249 } else if (pn.getChild("literal") != null) {
1250 return parse_literal(pn.getChild("literal"));
1251 } else if (pn.getChild("operator") != null) {
1252 return parse_operator(pn.getChild("operator"));
1253 } else if (pn.getChild("relation") != null) {
1254 return parse_relation(pn.getChild("relation"));
1255 } else if (pn.getChild("sizeof") != null) {
1256 return parse_sizeof(pn.getChild("sizeof"));
1257 } else if (pn.getChild("simple_expr") != null) {
1258 return parse_simple_expr(pn.getChild("simple_expr"));
1259 } else if (pn.getChild("elementof") != null) {
1260 return parse_elementof(pn.getChild("elementof"));
1261 } else if (pn.getChild("tupleof") != null) {
1262 return parse_tupleof(pn.getChild("tupleof"));
1263 } else if (pn.getChild("isvalid") != null) {
1264 er.report(pn, "Operation 'isvalid' is currently unsupported.");
1267 er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
1272 private Expr parse_elementof(ParseNode pn) {
1273 if (!precheck(pn, "elementof")) {
1278 String setname = pn.getChild("name").getTerminal();
1279 assert setname != null;
1280 SetDescriptor sd = lookupSet(setname);
1283 er.report(pn, "Undefined set '" + setname + "'");
1287 /* get left side expr */
1288 Expr expr = parse_expr(pn.getChild("expr"));
1294 return new ElementOfExpr(expr, sd);
1297 private Expr parse_tupleof(ParseNode pn) {
1298 if (!precheck(pn, "tupleof")) {
1303 String relname = pn.getChild("name").getTerminal();
1304 assert relname != null;
1305 RelationDescriptor rd = lookupRelation(relname);
1308 er.report(pn, "Undefined relation '" + relname + "'");
1312 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1313 Expr right = parse_expr(pn.getChild("right").getChild("expr"));
1315 if ((left == null) || (right == null)) {
1319 return new TupleOfExpr(left, right, rd);
1322 private Expr parse_simple_expr(ParseNode pn) {
1323 if (!precheck(pn, "simple_expr")) {
1327 // only locations so far
1328 return parse_location(pn.getChild("location"));
1331 private Expr parse_location(ParseNode pn) {
1332 if (!precheck(pn, "location")) {
1336 if (pn.getChild("var") != null) {
1337 // should be changed into a namespace check */
1338 return new VarExpr(pn.getChild("var").getTerminal());
1339 } else if (pn.getChild("cast") != null) {
1340 return parse_cast(pn.getChild("cast"));
1341 } else if (pn.getChild("dot") != null) {
1342 return parse_dot(pn.getChild("dot"));
1344 throw new IRException();
1348 private RelationExpr parse_relation(ParseNode pn) {
1349 if (!precheck(pn, "relation")) {
1353 RelationExpr re = new RelationExpr();
1355 /* get quantitifer var */
1356 VarDescriptor vd = parse_quantifiervar(pn.getChild("quantifiervar"));
1365 /* grab list of relations */
1366 ParseNodeVector relations = pn.getChild("relations").getChildren();
1367 assert relations.size() >= 1;
1369 // #TBD#: verify that the relations are in the correct order and that the
1370 // first relation is getting the correct "inv" assigned from "expr"
1372 /* lets verify that these relations are defined */
1373 for (int i = 0; i < relations.size(); i++) {
1374 ParseNode rn = relations.elementAt(i);
1375 String relname = rn.getLabel();
1376 boolean inverse = rn.getChild("inv") != null;
1378 RelationDescriptor relation = lookupRelation(relname);
1380 if (relation == null) {
1381 /* Semantic Error: relation not definied" */
1382 er.report(rn, "Undefined relation '" + relname + "'");
1386 re.setRelation(relation, inverse);
1388 /* if we are not at end of list then create new relation and
1389 replace it to chain the relations */
1390 if (i + 1 < relations.size()) {
1391 re = new RelationExpr(re); // should create relation with domain as older 're'
1398 private SizeofExpr parse_sizeof(ParseNode pn) {
1399 if (!precheck(pn, "sizeof")) {
1404 SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
1406 if (setexpr == null) {
1410 return new SizeofExpr(setexpr);
1413 private CastExpr parse_cast(ParseNode pn) {
1414 if (!precheck(pn, "cast")) {
1419 String typename = pn.getChild("type").getTerminal();
1420 assert typename != null;
1421 TypeDescriptor type = lookupType(typename);
1424 /* semantic error: undefined type in cast */
1425 er.report(pn, "Undefined type '" + typename + "' in cast operator");
1430 Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
1436 return new CastExpr(type, expr);
1439 private SetExpr parse_setexpr(ParseNode pn) {
1440 if (!precheck(pn, "setexpr")) {
1444 // #TBD#: setexpr and parse_relation seem to be cousins... is there a reduction/refactor possible?
1446 if (pn.getChild("set") != null) {
1447 String setname = pn.getChild("set").getTerminal();
1448 assert setname != null;
1449 SetDescriptor sd = lookupSet(setname);
1452 er.report(pn, "Unknown or undefined set '" + setname + "'");
1455 return new SetExpr(sd);
1457 } else if (pn.getChild("dot") != null) {
1458 VarDescriptor vd = parse_quantifiervar(pn.getChild("dot").getChild("quantifiervar"));
1459 RelationDescriptor relation = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
1460 return new ImageSetExpr(vd, relation);
1461 } else if (pn.getChild("dotinv") != null) {
1462 VarDescriptor vd = parse_quantifiervar(pn.getChild("dotinv").getChild("quantifiervar"));
1463 RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
1464 return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
1466 throw new IRException();
1470 private VarDescriptor parse_quantifiervar(ParseNode pn) {
1471 if (!precheck(pn, "quantifiervar")) {
1476 String varname = pn.getTerminal();
1477 assert varname != null;
1479 /* NOTE: quantifier var's are only found in the constraints and
1480 model definitions... therefore we can do a semantic check here
1481 to make sure that the variables exist in the symbol table */
1483 /* NOTE: its assumed that the symbol table stack is appropriately
1484 set up with the parent quantifier symbol table */
1485 assert !sts.empty();
1487 /* do semantic check and if valid, add it to symbol table
1488 and add it to the quantifier as well */
1489 if (sts.peek().contains(varname)) {
1490 return new VarDescriptor(varname);
1492 /* Semantic Error: undefined variable */
1493 er.report(pn, "Undefined variable '" + varname + "'");
1498 private LiteralExpr parse_literal(ParseNode pn) {
1499 if (!precheck(pn, "literal")) {
1503 if (pn.getChild("boolean") != null) {
1504 if (pn.getChild("boolean").getChild("true") != null) {
1505 return new BooleanLiteralExpr(true);
1507 return new BooleanLiteralExpr(false);
1509 } else if (pn.getChild("decimal") != null) {
1510 String integer = pn.getChild("decimal").getTerminal();
1512 /* Check for integer literal overflow */
1513 BigInteger intLitBI = new BigInteger(integer);
1514 BigInteger intMax = new BigInteger("" + Integer.MAX_VALUE);
1515 BigInteger intMin = new BigInteger("" + Integer.MIN_VALUE);
1518 if (intLitBI.compareTo(intMin) < 0) {
1519 value = Integer.MIN_VALUE;
1520 er.warn(pn, "Integer literal overflow");
1521 } else if (intLitBI.compareTo(intMax) > 0) {
1522 value = Integer.MAX_VALUE;
1523 er.warn(pn, "Integer literal overflow");
1525 /* no truncation needed */
1526 value = Integer.parseInt(integer);
1529 return new IntegerLiteralExpr(value);
1530 } else if (pn.getChild("token") != null) {
1531 return new TokenLiteralExpr(pn.getChild("token").getTerminal());
1532 } else if (pn.getChild("string") != null) {
1533 throw new IRException("string unsupported");
1534 } else if (pn.getChild("char") != null) {
1535 throw new IRException("char unsupported");
1537 throw new IRException("unknown literal expression type.");
1541 private OpExpr parse_operator(ParseNode pn) {
1542 if (!precheck(pn, "operator")) {
1546 String opname = pn.getChild("op").getTerminal();
1547 Opcode opcode = Opcode.decodeFromString(opname);
1549 if (opcode == null) {
1550 er.report(pn, "Unsupported operation: " + opname);
1554 Expr left = parse_expr(pn.getChild("left").getChild("expr"));
1557 if (pn.getChild("right") != null) {
1558 right = parse_expr(pn.getChild("right").getChild("expr"));
1565 if (right == null && opcode != Opcode.NOT) {
1566 er.report(pn, "Two arguments required.");
1570 return new OpExpr(opcode, left, right);
1573 private DotExpr parse_dot(ParseNode pn) {
1574 if (!precheck(pn, "dot")) {
1578 Expr left = parse_simple_expr(pn.getChild("simple_expr"));
1584 String field = pn.getChild("field").getTerminal();
1588 if (pn.getChild("index") != null) {
1589 index = parse_expr(pn.getChild("index").getChild("expr"));
1591 if (index == null) {
1596 return new DotExpr(left, field, index);