import java.util.*;
import java.math.BigInteger;
import MCC.State;
+import MCC.Compiler;
public class SemanticChecker {
StructureTypeDescriptor dCurrentType;
IRErrorReporter er;
-
+
public SemanticChecker () {
dCurrentType = null;
stTypes = null;
stGlobals = state.stGlobals;
sts = new SymbolTableStack();
-
+
// add int and bool to the types list
stTypes.add(ReservedTypeDescriptor.BIT);
stTypes.add(ReservedTypeDescriptor.BYTE);
stSets.add(new ReservedSetDescriptor("int", ReservedTypeDescriptor.INT));
stSets.add(new ReservedSetDescriptor("token", ReservedTypeDescriptor.INT));
- boolean ok = true;
+ boolean ok = true;
er.setFilename(state.infile + ".struct");
if (!parse_structures(state.ptStructures)) {
+
ok = false;
+ er.report(null, "Error parsing structs.");
}
er.setFilename(state.infile + ".space");
if (!parse_space(state.ptSpace)) {
ok = false;
+ er.report(null, "Error parsing sets and relations.");
}
-
+
er.setFilename(state.infile + ".constraints");
if (!parse_constraints(state.ptConstraints)) {
ok = false;
+ er.report(null, "Error parsing constraints.");
}
er.setFilename(state.infile + ".model");
if (!parse_rules(state.ptModel)) {
ok = false;
+ er.report(null, "Error parsing model definition rules.");
}
return ok;
}
- /********************** HELPER FUNCTIONS ************************/
+ /********************** HELPER FUNCTIONS ************************/
/**
- * special case lookup that returns null if no such type exists
+ * special case lookup that returns null if no such type exists
*/
private TypeDescriptor lookupType(String typename) {
return lookupType(typename, false);
*/
private TypeDescriptor lookupType(String typename, boolean createmissing) {
if (stTypes.get(typename) != null) {
- // the type exists, so plug in the descriptor directly
- return (TypeDescriptor) stTypes.get(typename);
+ // the type exists, so plug in the descriptor directly
+ return (TypeDescriptor) stTypes.get(typename);
} else if (createmissing) {
return new MissingTypeDescriptor(typename);
} else {
return null;
- }
+ }
}
/**
- * reserve a name
+ * reserve a name
*/
private VarDescriptor reserveName(ParseNode pn) {
assert pn != null;
String varname = pn.getTerminal();
assert varname != null;
-
+
/* do semantic check and if valid, add it to symbol table
and add it to the quantifier as well */
if (sts.peek().contains(varname)) {
}
/**
- * special case lookup that returns null if no such set exists
+ * special case lookup that returns null if no such set exists
*/
private SetDescriptor lookupSet(String setname) {
return lookupSet(setname, false);
*/
private SetDescriptor lookupSet(String setname, boolean createmissing) {
if (stSets.get(setname) != null) {
- // the set exists, so plug in the descriptor directly
- return (SetDescriptor) stSets.get(setname);
+ // the set exists, so plug in the descriptor directly
+ return (SetDescriptor) stSets.get(setname);
} else if (createmissing) {
return new MissingSetDescriptor(setname);
} else {
return null;
- }
+ }
}
-
+
/**
* does a look up in the set's symbol table. if the set is
* not found than a missing set descriptor is returned
*/
private RelationDescriptor lookupRelation(String relname) {
if (stRelations.get(relname) != null) {
- // the relation exists, so plug in the descriptor directly
- return (RelationDescriptor) stRelations.get(relname);
+ // the relation exists, so plug in the descriptor directly
+ return (RelationDescriptor) stRelations.get(relname);
} else {
return null;
- }
+ }
}
-
-
+
+
private static int count = 0;
- private boolean precheck(ParseNode pn, String label) {
+ private boolean precheck(ParseNode pn, String label) {
if (pn == null) {
er.report(pn, "IE: Expected '" + label + "', got null");
assert false;
return true;
}
- /********************* PARSING FUNCTIONS ************************/
+ /********************* PARSING FUNCTIONS ************************/
private boolean parse_rules(ParseNode pn) {
if (!precheck(pn, "rules")) {
boolean ok = true;
ParseNodeVector rules = pn.getChildren();
-
+
for (int i = 0; i < rules.size(); i++) {
ParseNode rule = rules.elementAt(i);
if (!parse_rule(rule)) {
+ er.report(rule, "Error parsing rule");
ok = false;
}
}
-
- /* type check */
+
+ /* type check */
Iterator ruleiterator = state.vRules.iterator();
-
+
while (ruleiterator.hasNext()) {
- Rule rule = (Rule) ruleiterator.next();
+ Rule rule = (Rule) ruleiterator.next();
Expr guard = rule.getGuardExpr();
final SymbolTable rulest = rule.getSymbolTable();
SemanticAnalyzer sa = new SemanticAnalyzer() {
public SymbolTable getSymbolTable() { return rulest; }
};
TypeDescriptor guardtype = guard.typecheck(sa);
-
+
if (guardtype == null) {
ok = false;
} else if (guardtype != ReservedTypeDescriptor.INT) {
er.report(null, "Type of guard must be 'int' not '" + guardtype.getSymbol() + "'");
ok = false;
}
-
+
if (!rule.getInclusion().typecheck(sa)) {
+ er.report(null, "Error typechecking rule:"+rule);
ok = false;
- }
-
+ }
+
Iterator quantifiers = rule.quantifiers();
-
+
while (quantifiers.hasNext()) {
Quantifier q = (Quantifier) quantifiers.next();
-
+
if (q instanceof ForQuantifier && !((ForQuantifier)q).typecheck(sa)) {
ok = false;
}
- }
- }
+ }
+ }
/* do any post checks ?? */
boolean ok = true;
Rule rule = new Rule();
-
+
/* get rule type */
boolean isstatic = pn.getChild("static") != null;
boolean isdelay = pn.getChild("delay") != null;
assert sts.empty();
sts.push(stGlobals);
sts.push(rule.getSymbolTable());
-
/* optional quantifiers */
if (pn.getChild("quantifiers") != null) {
ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
-
for (int i = 0; i < quantifiers.size(); i++) {
ParseNode qn = quantifiers.elementAt(i);
Quantifier quantifier = parse_quantifier(qn);
} else {
rule.addQuantifier(quantifier);
}
- }
+ }
}
-
+
/* get guard expr */
Expr guard = parse_expr(pn.getChild("expr"));
/* inclusion constraint */
Inclusion inclusion = parse_inclusion(pn.getChild("inclusion"));
-
+
if (inclusion == null) {
ok = false;
} else {
rule.setInclusion(inclusion);
}
-
+
/* pop symbol table stack */
SymbolTable st = sts.pop();
sts.pop(); /* pop off globals */
/* make sure the stack we pop is our rule s.t. */
- assert st == rule.getSymbolTable();
+ assert st == rule.getSymbolTable();
assert sts.empty();
/* add rule to global set */
if (pn.getChild("set") != null) {
ParseNode set = pn.getChild("set");
Expr expr = parse_expr(set.getChild("expr"));
-
+
if (expr == null) {
return null;
}
String setname = set.getChild("name").getTerminal();
assert setname != null;
SetDescriptor sd = lookupSet(setname);
-
+
if (sd == null) {
er.report(set.getChild("name"), "Undefined set '" + setname + "'");
return null;
ParseNode relation = pn.getChild("relation");
Expr leftexpr = parse_expr(relation.getChild("left").getChild("expr"));
Expr rightexpr = parse_expr(relation.getChild("right").getChild("expr"));
-
+
if ((leftexpr == null) || (rightexpr == null)) {
return null;
}
if (!precheck(pn, "constraints")) {
return false;
}
+ //System.out.println(pn.PPrint(2,true));
boolean ok = true;
ParseNodeVector constraints = pn.getChildren();
-
+
for (int i = 0; i < constraints.size(); i++) {
ParseNode constraint = constraints.elementAt(i);
assert constraint.getLabel().equals("constraint");
/* do any post checks... (type constraints, etc?) */
+ Iterator consiterator = state.vConstraints.iterator();
+
+ while (consiterator.hasNext()) {
+ Constraint cons = (Constraint) consiterator.next();
+
+ final SymbolTable consst = cons.getSymbolTable();
+ SemanticAnalyzer sa = new SemanticAnalyzer() {
+ public IRErrorReporter getErrorReporter() { return er; }
+ public SymbolTable getSymbolTable() { return consst; }
+ };
+
+ TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
+
+ if (constype == null) {
+ System.out.println("Failed attempting to type constraint");
+ ok = false;
+ } else if (constype != ReservedTypeDescriptor.INT) {
+ er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
+ ok = false;
+ }
+ }
+
return ok;
}
/* set up symbol table for constraint */
assert sts.empty();
sts.push(constraint.getSymbolTable());
-
+
/* get quantifiers */
if (pn.getChild("quantifiers") != null) {
ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
-
+
for (int i = 0; i < quantifiers.size(); i++) {
ParseNode qn = quantifiers.elementAt(i);
assert qn.getLabel().equals("quantifier");
Quantifier quantifier = parse_quantifier(qn);
if (quantifier == null) {
+ System.out.println("Failed parsing quantifier");
ok = false;
} else {
constraint.addQuantifier(quantifier);
}
}
}
-
+
/* get body */
LogicStatement logicexpr = parse_body(pn.getChild("body"));
if (logicexpr == null) {
+ System.out.println("Failed parsing logical expression");
ok = false;
} else {
constraint.setLogicStatement(logicexpr);
}
-
+
/* pop symbol table stack */
SymbolTable st = sts.pop();
/* make sure the stack we pop is our constraint s.t. */
- assert st == constraint.getSymbolTable();
+ assert st == constraint.getSymbolTable();
assert sts.empty();
/* add to vConstraints */
- vConstraints.addElement(constraint);
+ vConstraints.addElement(constraint);
return ok;
}
private Quantifier parse_quantifier(ParseNode pn) {
if (!precheck(pn, "quantifier")) {
- return null;
+ return null;
}
if (pn.getChild("forall") != null) { /* forall element in Set */
/* get var */
VarDescriptor vd = reserveName(pn.getChild("var"));
-
+
if (vd == null) {
return null;
- }
+ }
sq.setVar(vd);
SetDescriptor set = parse_set(pn.getChild("set"));
assert set != null;
sq.setSet(set);
+ vd.setSet(set);
vd.setType(set.getType());
/* get vars */
VarDescriptor vd1 = reserveName(pn.getChild("left"));
VarDescriptor vd2 = reserveName(pn.getChild("right"));
-
+
if ((vd1 == null) || (vd2 == null)) {
return null;
}
-
+
rq.setTuple(vd1, vd2);
-
+
/* get relation */
String relationname = pn.getChild("relation").getTerminal();
assert relationname != null;
if (rd == null) {
return null;
}
-
+
+ rd.addUsage(RelationDescriptor.IMAGE);
rq.setRelation(rd);
vd1.setType(rd.getDomain().getType());
+ vd1.setSet(rd.getDomain());
vd2.setType(rd.getRange().getType());
+ vd2.setSet(rd.getRange());
return rq;
} else if (pn.getChild("for") != null) { /* for j = x to y */
ForQuantifier fq = new ForQuantifier();
-
+
/* grab var */
VarDescriptor vd = reserveName(pn.getChild("var"));
return null;
}
+ vd.setSet(lookupSet("int", false));
vd.setType(ReservedTypeDescriptor.INT);
fq.setVar(vd);
Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
+
if ((lower == null) || (upper == null)) {
return null;
}
-
+ vd.setBounds(lower,upper);
fq.setBounds(lower, upper);
return fq;
private LogicStatement parse_body(ParseNode pn) {
if (!precheck(pn, "body")) {
- return null;
+ return null;
}
-
+
if (pn.getChild("and") != null) {
/* body AND body */
LogicStatement left, right;
left = parse_body(pn.getChild("and").getChild("left").getChild("body"));
right = parse_body(pn.getChild("and").getChild("right").getChild("body"));
-
+
if ((left == null) || (right == null)) {
return null;
}
-
+
// what do we want to call the and/or/not body classes?
return new LogicStatement(LogicStatement.AND, left, right);
} else if (pn.getChild("or") != null) {
LogicStatement left, right;
left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
-
+
if ((left == null) || (right == null)) {
return null;
}
} else if (pn.getChild("not") != null) {
/* NOT body */
LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
-
if (left == null) {
return null;
}
-
+
return new LogicStatement(LogicStatement.NOT, left);
} else if (pn.getChild("predicate") != null) {
return parse_predicate(pn.getChild("predicate"));
} else {
throw new IRException();
- }
+ }
}
private Predicate parse_predicate(ParseNode pn) {
if (pn.getChild("inclusion") != null) {
ParseNode in = pn.getChild("inclusion");
-
+
/* Expr */
Expr expr = parse_expr(in.getChild("expr"));
-
- if (expr == null) {
+
+ if (expr == null) {
return null;
}
return new InclusionPredicate(expr, setexpr);
} else if (pn.getChild("expr") != null) {
Expr expr = parse_expr(pn.getChild("expr"));
-
+
if (expr == null) {
return null;
}
return new ExprPredicate(expr);
} else {
throw new IRException();
- }
+ }
}
private SetDescriptor parse_set(ParseNode pn) {
if (!precheck(pn, "set")) {
return null;
}
-
+
if (pn.getChild("name") != null) {
String setname = pn.getChild("name").getTerminal();
assert setname != null;
-
+
if (!stSets.contains(setname)) {
/* Semantic Error: unknown set */
er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
SetDescriptor sd = (SetDescriptor) stSets.get(setname);
assert sd != null;
return sd;
- }
- } else if (pn.getChild("listofliterals") != null) {
+ }
+ } else if (pn.getChild("listofliterals") != null) {
TokenSetDescriptor tokenset = new TokenSetDescriptor();
ParseNodeVector token_literals = pn.getChild("listofliterals").getChildren();
assert token_literals.size() > 0;
-
+
for (int i = 0; i < token_literals.size(); i++) {
ParseNode literal = token_literals.elementAt(i);
assert literal.getLabel().equals("literal");
if (litexpr == null) {
return null;
}
-
+
if (litexpr instanceof TokenLiteralExpr || litexpr instanceof IntegerLiteralExpr) {
tokenset.addLiteral(litexpr);
} else {
er.report(literal, "Elements of a user-defined set must be of type token or integer");
// return null; /* don't think we need to return null */
}
- }
+ }
return tokenset;
} else {
throw new IRException(pn.getTerminal());
}
}
-
+
private boolean parse_space(ParseNode pn) {
if (!precheck(pn, "space")) {
return false;
}
-
+
boolean ok = true;
ParseNodeVector sets = pn.getChildren("setdefinition");
ParseNodeVector relations = pn.getChildren("relationdefinition");
assert pn.getChildren().size() == (sets.size() + relations.size());
-
+
/* parse sets */
for (int i = 0; i < sets.size(); i++) {
if (!parse_setdefinition(sets.elementAt(i))) {
// for cycles etc.
// #TBD#: typecheck and check for cycles
-
+
/* replace missing with actual */
Iterator allsets = state.stSets.descriptors();
-
+
while (allsets.hasNext()) {
SetDescriptor sd = (SetDescriptor) allsets.next();
Vector subsets = sd.getSubsets();
for (int i = 0; i < subsets.size(); i++) {
SetDescriptor subset = (SetDescriptor) subsets.elementAt(i);
-
+
if (subset instanceof MissingSetDescriptor) {
SetDescriptor newsubset = lookupSet(subset.getSymbol());
}
}
}
-
+
return ok;
}
if (!precheck(pn, "setdefinition")) {
return false;
}
-
+
boolean ok = true;
-
+
/* get set name */
String setname = pn.getChild("name").getTerminal();
assert (setname != null);
SetDescriptor sd = new SetDescriptor(setname);
-
+
/* get set type */
String settype = pn.getChild("type").getTerminal();
TypeDescriptor type = lookupType(settype);
if (type == null) {
er.report(pn, "Undefined type '" + settype + "'");
- ok = false;
+ ok = false;
} else {
sd.setType(type);
}
/* is this a partition? */
boolean partition = pn.getChild("partition") != null;
- sd.isPartition(partition);
+ sd.isPartition(partition);
/* if set has subsets, add them to set descriptor */
if (pn.getChild("setlist") != null) {
ParseNodeVector setlist = pn.getChild("setlist").getChildren();
-
+
for (int i = 0; i < setlist.size(); i++) {
String subsetname = setlist.elementAt(i).getLabel();
sd.addSubset(lookupSet(subsetname, CREATE_MISSING));
- }
+ }
}
/* add set to symbol table */
assert rangesetname != null;
/* get domain multiplicity */
- String domainmult = pn.getChild("domain").getChild("mult").getTerminal();
- assert domainmult != null;
+ String domainmult;
+ if (pn.getChild("domain").getChild("domainmult") != null)
+ domainmult = pn.getChild("domain").getChild("domainmult").getChild("mult").getTerminal();
+ //assert domainmult != null;
/* get range multiplicity */
- String rangemult = pn.getChild("range").getChild("mult").getTerminal();
- assert rangemult != null;
+ String rangemult;
+ if (pn.getChild("range").getChild("domainrange") != null)
+ rangemult = pn.getChild("range").getChild("domainrange").getChild("mult").getTerminal();
+ //assert rangemult != null;
- /* NOTE: it is assumed that the sets have been parsed already so that the
+ /* NOTE: it is assumed that the sets have been parsed already so that the
set namespace is fully populated. any missing setdescriptors for the set
symbol table will be assumed to be errors and reported. */
if (!precheck(pn, "structures")) {
return false;
}
-
+
boolean ok = true;
ParseNodeVector structures = pn.getChildren("structure");
}
}
- // ok, all the structures have been parsed, now we gotta type check
+ // ok, all the structures have been parsed, now we gotta type check
Enumeration types = stTypes.getDescriptors();
while (types.hasMoreElements()) {
if (t instanceof ReservedTypeDescriptor) {
// we don't need to check reserved types
} else if (t instanceof StructureTypeDescriptor) {
-
+
StructureTypeDescriptor type = (StructureTypeDescriptor) t;
TypeDescriptor subtype = type.getSuperType();
Iterator fields = type.getFields();
while (fields.hasNext()) {
- FieldDescriptor field = (FieldDescriptor) fields.next();
+ FieldDescriptor field = (FieldDescriptor) fields.next();
TypeDescriptor fieldtype = field.getType();
assert fieldtype != null;
if (newtype == null) {
// type never defined
// #TBD#: replace new ParseNode with original parsenode
- er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
- ok = false;
+
+ if (!field.getPtr()) {
+ /* Pointer types don't have to be defined */
+ er.report(null, "Undefined type '" + fieldtype.getSymbol() + "'");
+ ok = false;
+ }
} else {
assert newtype != null;
field.setType(newtype);
}
- }
+ }
}
Iterator labels = type.getLabels();
}
}
}
-
+
} else {
throw new IRException("shouldn't be any other typedescriptor classes");
}
if (t instanceof ReservedTypeDescriptor) {
// we don't need to check reserved types
} else if (t instanceof StructureTypeDescriptor) {
-
+
StructureTypeDescriptor type = (StructureTypeDescriptor)t;
TypeDescriptor subtype = type.getSuperType();
Iterator fields = type.getFields();
while (fields.hasNext()) {
- FieldDescriptor field = (FieldDescriptor) fields.next();
+ FieldDescriptor field = (FieldDescriptor) fields.next();
if (field instanceof ArrayDescriptor) {
ArrayDescriptor ad = (ArrayDescriptor) field;
public IRErrorReporter getErrorReporter() { return er; }
public SymbolTable getSymbolTable() { return stGlobals; }
});
+ if (Compiler.REJECTLENGTH) {
+ analyze_length(indexbound);
+ }
+
if (indextype == null) {
ok = false;
public IRErrorReporter getErrorReporter() { return er; }
public SymbolTable getSymbolTable() { return stGlobals; }
});
-
+
if (indextype != ReservedTypeDescriptor.INT) {
er.report(null, "Label '" + type.getSymbol() + "." + label.getSymbol() + "' index must be type 'int' not '" + indextype.getSymbol() + "'");
ok = false;
}
}
}
-
- } else {
+ } else {
throw new IRException("shouldn't be any other typedescriptor classes");
}
-
}
// #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
- // subtypes, of course, are not real subtypes, they are merely a way to validate a
+ // subtypes, of course, are not real subtypes, they are merely a way to validate a
// cast, i believe
return ok;
}
+ private void analyze_length(Expr indexbound) {
+ Set descriptors=indexbound.getRequiredDescriptors();
+ for(Iterator it=descriptors.iterator();it.hasNext();) {
+ Descriptor d=(Descriptor)it.next();
+ if (d instanceof FieldDescriptor) {
+ state.noupdate.add(d);
+ } else if (d instanceof ArrayDescriptor) {
+ state.noupdate.add(d);
+ } else if (d instanceof VarDescriptor) {
+ state.noupdate.add(d);
+ }
+ }
+ }
+
private boolean parse_global(ParseNode pn) {
if (!precheck(pn, "global")) {
return false;
String type = pn.getChild("type").getTerminal();
assert type != null;
+
TypeDescriptor td = lookupType(type);
assert td != null;
- assert !(td instanceof ReservedTypeDescriptor);
-
+
if (stGlobals.contains(name)) {
/* redefinition of global */
er.report(pn, "Redefinition of global '" + name + "'");
boolean ok = true;
String typename = pn.getChild("name").getTerminal();
StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
-
+
if (pn.getChild("subtype") != null) {
// has a subtype, lets try to resolve it
String subtype = pn.getChild("subtype").getTerminal();
/* lookup the type to get the type descriptor */
type.setSuperType(lookupType(subtype, CREATE_MISSING));
+ } else if (pn.getChild("subclass") != null) {
+ // has a subtype, lets try to resolve it
+ String subclass = pn.getChild("subclass").getTerminal();
+
+ if (subclass.equals(typename)) {
+ // Semantic Error: cyclic inheritance
+ er.report(pn, "Cyclic inheritance prohibited");
+ ok = false;
+ }
+
+ /* lookup the type to get the type descriptor */
+ type.setSuperType(lookupType(subclass, CREATE_MISSING));
+ type.setSubClass(true);
}
// set the current type so that the recursive parses on the labels
- // and fields can add themselves automatically to the current type
+ // and fields can add themselves automatically to the current type
dCurrentType = type;
-
+
// parse the labels and fields
- if (!parse_labelsandfields(pn.getChild("lf"))) {
+ if (pn.getChild("lf")!=null && !parse_labelsandfields(pn.getChild("lf"))) {
ok = false;
}
} else {
stTypes.add(type);
}
-
+
return ok;
}
}
boolean ok = true;
-
- // check the fields first (need the field names
+
+ // check the fields first (need the field names
// to type check the labels)
if (!parse_fields(pn.getChild("fields"))) {
ok = false;
if (!precheck(pn, "fields")) {
return false;
}
-
+
boolean ok = true;
-
+
/* NOTE: because the order of the fields is important when defining a data structure,
and because the order is defined by the order of the fields defined in the field
vector, its important that the parser returns the fields in the correct order */
-
+
ParseNodeVector fields = pn.getChildren();
for (int i = 0; i < fields.size(); i++) {
- ParseNode field = fields.elementAt(i);
+ ParseNode field = fields.elementAt(i);
FieldDescriptor fd;
boolean reserved;
String name = null;
fd = new ReservedFieldDescriptor();
reserved = true;
} else {
- name = field.getChild("name").getTerminal();
+ name = field.getChild("name").getTerminal();
fd = new FieldDescriptor(name);
reserved = false;
}
fd.setType(lookupType(type, CREATE_MISSING));
if (field.getChild("index") != null) {
- // field is an array, so create an array descriptor to wrap the
+ // field is an array, so create an array descriptor to wrap the
// field descriptor and then replace the top level field descriptor with
// this array descriptor
Expr expr = parse_expr(field.getChild("index").getChild("expr"));
// #ATTN#: do we really want to return an exception here?
throw new IRException("invalid index expression");
}
- ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
+ ArrayDescriptor ad = new ArrayDescriptor(fd, expr);
fd = ad;
}
if (reserved == false) {
// lets double check that we are redefining a field
if (dCurrentType.getField(name) != null) {
- // Semantic Error: field redefinition
+ // Semantic Error: field redefinition
er.report(pn, "Redefinition of field '" + name + "'");
ok = false;
} else {
dCurrentType.addField(fd);
}
}
-
+
return ok;
}
ParseNodeVector labels = pn.getChildren();
- for (int i = 0; i < labels.size(); i++) {
+ for (int i = 0; i < labels.size(); i++) {
ParseNode label = labels.elementAt(i);
String name = label.getChild("name").getTerminal();
- LabelDescriptor ld = new LabelDescriptor(name);
+ LabelDescriptor ld = new LabelDescriptor(name);
if (label.getChild("index") != null) {
Expr expr = parse_expr(label.getChild("index").getChild("expr"));
/* #ATTN#: do we really want to return an exception here? */
throw new IRException("Invalid expression");
}
- ld.setIndex(expr);
- }
-
+ ld.setIndex(expr);
+ }
+
String type = label.getChild("type").getTerminal();
ld.setType(lookupType(type, CREATE_MISSING));
-
- String field = label.getChild("field").getTerminal();
+
+ String field = label.getChild("field").getTerminal();
FieldDescriptor fd = dCurrentType.getField(field);
if (fd == null) {
er.report(pn, "Redefinition of label '" + name + "'");
ok = false;
} else {
- dCurrentType.addLabel(ld);
+ dCurrentType.addLabel(ld);
}
}
// we've got a variable reference... we'll have to scope check it later
// when we are completely done... there are also some issues of cyclic definitions
return new VarExpr(pn.getChild("var").getTerminal());
+ } else if (pn.getChild("sumexpr") != null) {
+ return parse_sum(pn.getChild("sumexpr"));
} else if (pn.getChild("literal") != null) {
return parse_literal(pn.getChild("literal"));
} else if (pn.getChild("operator") != null) {
} else if (pn.getChild("sizeof") != null) {
return parse_sizeof(pn.getChild("sizeof"));
} else if (pn.getChild("simple_expr") != null) {
- return parse_simple_expr(pn.getChild("simple_expr"));
+ return parse_simple_expr(pn.getChild("simple_expr"));
} else if (pn.getChild("elementof") != null) {
- return parse_elementof(pn.getChild("elementof"));
+ return parse_elementof(pn.getChild("elementof"));
} else if (pn.getChild("tupleof") != null) {
- return parse_tupleof(pn.getChild("tupleof"));
+ return parse_tupleof(pn.getChild("tupleof"));
} else if (pn.getChild("isvalid") != null) {
er.report(pn, "Operation 'isvalid' is currently unsupported.");
return null;
} else {
er.report(pn, "Unknown or invalid expression type '" + pn.getTerminal() + "'");
return null;
- }
+ }
}
private Expr parse_elementof(ParseNode pn) {
/* get left side expr */
Expr expr = parse_expr(pn.getChild("expr"));
-
+
if (expr == null) {
return null;
}
if (!precheck(pn, "tupleof")) {
return null;
}
-
+
/* get relation */
String relname = pn.getChild("name").getTerminal();
assert relname != null;
String relname = pn.getChild("name").getTerminal();
boolean inverse = pn.getChild("inv") != null;
- Expr expr = parse_expr(pn.getChild("expr"));
+ Expr expr = parse_expr(pn.getChild("expr"));
if (expr == null) {
return null;
}
-
+
RelationDescriptor relation = lookupRelation(relname);
-
+
if (relation == null) {
/* Semantic Error: relation not definied" */
er.report(pn, "Undefined relation '" + relname + "'");
return null;
- }
+ }
/* add usage so correct sets are created */
relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
-
+
return new RelationExpr(expr, relation, inverse);
}
/* get setexpr */
SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
-
+
if (setexpr == null) {
return null;
}
return new SizeofExpr(setexpr);
}
+ private SumExpr parse_sum(ParseNode pn) {
+ if (!precheck(pn, "sumexpr")) {
+ return null;
+ }
+ String setname = pn.getChild("dot").getChild("set").getTerminal();
+ assert setname != null;
+ SetDescriptor sd = lookupSet(setname);
+
+ if (sd == null) {
+ er.report(pn, "Unknown or undefined set '" + setname + "'");
+ return null;
+ }
+
+ RelationDescriptor rd = lookupRelation(pn.getChild("dot").getChild("relation").getTerminal());
+ rd.addUsage(RelationDescriptor.IMAGE);
+
+ return new SumExpr(sd,rd);
+ }
+
private CastExpr parse_cast(ParseNode pn) {
if (!precheck(pn, "cast")) {
return null;
/* semantic error: undefined type in cast */
er.report(pn, "Undefined type '" + typename + "' in cast operator");
return null;
- }
+ }
/* get expr */
Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
-
+
if (expr == null) {
return null;
- }
+ }
return new CastExpr(type, expr);
}
SetDescriptor sd = lookupSet(setname);
if (sd == null) {
- er.report(pn, "Unknown or undefined set '" + setname + "'");
+ er.report(pn, "Unknown or undefined set '" + setname + "'");
return null;
- } else {
+ } else {
return new SetExpr(sd);
}
} else if (pn.getChild("dot") != null) {
RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
relation.addUsage(RelationDescriptor.INVIMAGE);
return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
+ } else if (pn.getChild("dotset") != null) {
+ ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotset").getChild("setexpr"));
+ RelationDescriptor relation = lookupRelation(pn.getChild("dotset").getChild("relation").getTerminal());
+ relation.addUsage(RelationDescriptor.IMAGE);
+ return new ImageSetExpr(ise, relation);
+ } else if (pn.getChild("dotinvset") != null) {
+ ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotinvset").getChild("setexpr"));
+ RelationDescriptor relation = lookupRelation(pn.getChild("dotinvset").getChild("relation").getTerminal());
+ relation.addUsage(RelationDescriptor.INVIMAGE);
+ return new ImageSetExpr(ImageSetExpr.INVERSE, ise, relation);
} else {
throw new IRException();
}
/* get var */
String varname = pn.getTerminal();
assert varname != null;
-
+
/* NOTE: quantifier var's are only found in the constraints and
- model definitions... therefore we can do a semantic check here
+ model definitions... therefore we can do a semantic check here
to make sure that the variables exist in the symbol table */
/* NOTE: its assumed that the symbol table stack is appropriately
set up with the parent quantifier symbol table */
- assert !sts.empty();
+ assert !sts.empty();
/* do semantic check and if valid, add it to symbol table
and add it to the quantifier as well */
if (sts.peek().contains(varname)) {
- return new VarDescriptor(varname);
+ VarDescriptor vdold=(VarDescriptor)sts.peek().get(varname);
+ return vdold;
+ /* Dan was creating a new VarDescriptor...This seems
+ like the wrong thing to do. We'll just lookup the
+ other one.
+ --------------------------------------------------
+ VarDescriptor vd=new VarDescriptor(varname);
+ vd.setSet(vdold.getSet()); return vd;*/
} else {
/* Semantic Error: undefined variable */
er.report(pn, "Undefined variable '" + varname + "'");
return null;
}
}
-
+
private LiteralExpr parse_literal(ParseNode pn) {
if (!precheck(pn, "literal")) {
return null;
return new BooleanLiteralExpr(true);
} else {
return new BooleanLiteralExpr(false);
- }
- } else if (pn.getChild("decimal") != null) {
+ }
+ } else if (pn.getChild("decimal") != null) {
String integer = pn.getChild("decimal").getTerminal();
/* Check for integer literal overflow */
private OpExpr parse_operator(ParseNode pn) {
if (!precheck(pn, "operator")) {
- return null;
+ return null;
}
String opname = pn.getChild("op").getTerminal();
er.report(pn, "Unsupported operation: " + opname);
return null;
}
-
+
Expr left = parse_expr(pn.getChild("left").getChild("expr"));
Expr right = null;
-
+
if (pn.getChild("right") != null) {
right = parse_expr(pn.getChild("right").getChild("expr"));
}
- if (left == null) {
+ if (left == null) {
return null;
}
if (pn.getChild("index") != null) {
index = parse_expr(pn.getChild("index").getChild("expr"));
-
+
if (index == null) {
return null;
}
}
- return new DotExpr(left, field, index);
+ return new DotExpr(left, field, index);
}
}
-
projects / repair.git / blobdiff