projects / repair.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Small changes to allow:
[repair.git] / Repair / RepairCompiler / MCC / IR / SemanticChecker.java
diff --git a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
index e94f7bd124a3fe7ed823df21d28209f6b8a96ee7..af4aa96f735965afc163e8f8476aea5e86be3ff8 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
+++ b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
@@ -23,7 +23,7 @@ public class SemanticChecker {
     StructureTypeDescriptor dCurrentType;
 
     IRErrorReporter er;
     StructureTypeDescriptor dCurrentType;
 
     IRErrorReporter er;
-    
+
     public SemanticChecker () {
         dCurrentType = null;
        stTypes = null;
     public SemanticChecker () {
         dCurrentType = null;
        stTypes = null;
@@ -64,7 +64,7 @@ public class SemanticChecker {
         stGlobals = state.stGlobals;
 
         sts = new SymbolTableStack();
         stGlobals = state.stGlobals;
 
         sts = new SymbolTableStack();
-       
+
        // add int and bool to the types list
        stTypes.add(ReservedTypeDescriptor.BIT);
        stTypes.add(ReservedTypeDescriptor.BYTE);
        // add int and bool to the types list
        stTypes.add(ReservedTypeDescriptor.BIT);
        stTypes.add(ReservedTypeDescriptor.BYTE);
@@ -74,35 +74,40 @@ public class SemanticChecker {
         stSets.add(new ReservedSetDescriptor("int", ReservedTypeDescriptor.INT));
         stSets.add(new ReservedSetDescriptor("token", ReservedTypeDescriptor.INT));
 
         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)) {
 
         er.setFilename(state.infile + ".struct");
         if (!parse_structures(state.ptStructures)) {
+
             ok = false;
             ok = false;
+            er.report(null, "Error parsing structs.");
         }
 
         er.setFilename(state.infile + ".space");
         if (!parse_space(state.ptSpace)) {
             ok = false;
         }
 
         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.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.setFilename(state.infile + ".model");
         if (!parse_rules(state.ptModel)) {
             ok = false;
+            er.report(null, "Error parsing model definition rules.");
         }
 
         return ok;
     }
 
         }
 
         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) {
         return lookupType(typename, false);
@@ -114,23 +119,23 @@ public class SemanticChecker {
      */
     private TypeDescriptor lookupType(String typename, boolean createmissing) {
         if (stTypes.get(typename) != null) {
      */
     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;
         } 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;
      */
     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)) {
         /* do semantic check and if valid, add it to symbol table
            and add it to the quantifier as well */
         if (sts.peek().contains(varname)) {
@@ -145,7 +150,7 @@ public class SemanticChecker {
     }
 
     /**
     }
 
     /**
-     * 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) {
         return lookupSet(setname, false);
@@ -157,31 +162,31 @@ public class SemanticChecker {
      */
     private SetDescriptor lookupSet(String setname, boolean createmissing) {
         if (stSets.get(setname) != null) {
      */
     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;
         } 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) {
     /**
      * 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;
         } else {
             return null;
-        }       
+        }
     }
     }
-    
-    
+
+
     private static int count = 0;
     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;
        if (pn == null) {
             er.report(pn, "IE: Expected '" + label + "', got null");
             assert false;
@@ -201,7 +206,7 @@ public class SemanticChecker {
        return true;
     }
 
        return true;
     }
 
-    /********************* PARSING FUNCTIONS ************************/ 
+    /********************* PARSING FUNCTIONS ************************/
 
     private boolean parse_rules(ParseNode pn) {
         if (!precheck(pn, "rules")) {
 
     private boolean parse_rules(ParseNode pn) {
         if (!precheck(pn, "rules")) {
@@ -210,19 +215,20 @@ public class SemanticChecker {
 
         boolean ok = true;
         ParseNodeVector rules = pn.getChildren();
 
         boolean ok = true;
         ParseNodeVector rules = pn.getChildren();
-        
+
         for (int i = 0; i < rules.size(); i++) {
             ParseNode rule = rules.elementAt(i);
             if (!parse_rule(rule)) {
         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;
             }
         }
                 ok = false;
             }
         }
-               
-        /* type check */       
+
+        /* type check */
         Iterator ruleiterator = state.vRules.iterator();
         Iterator ruleiterator = state.vRules.iterator();
-        
+
         while (ruleiterator.hasNext()) {
         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() {
             Expr guard = rule.getGuardExpr();
             final SymbolTable rulest = rule.getSymbolTable();
             SemanticAnalyzer sa = new SemanticAnalyzer() {
@@ -230,28 +236,29 @@ public class SemanticChecker {
                     public SymbolTable getSymbolTable() { return rulest; }
                 };
             TypeDescriptor guardtype = guard.typecheck(sa);
                     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 (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)) {
             if (!rule.getInclusion().typecheck(sa)) {
+                er.report(null, "Error typechecking rule:"+rule);
                 ok = false;
                 ok = false;
-            }           
-            
+            }
+
             Iterator quantifiers = rule.quantifiers();
             Iterator quantifiers = rule.quantifiers();
-            
+
             while (quantifiers.hasNext()) {
                 Quantifier q = (Quantifier) quantifiers.next();
             while (quantifiers.hasNext()) {
                 Quantifier q = (Quantifier) quantifiers.next();
-                
+
                 if (q instanceof ForQuantifier && !((ForQuantifier)q).typecheck(sa)) {
                     ok = false;
                 }
                 if (q instanceof ForQuantifier && !((ForQuantifier)q).typecheck(sa)) {
                     ok = false;
                 }
-            }              
-        }        
+            }
+        }
 
         /* do any post checks ?? */
 
 
         /* do any post checks ?? */
 
@@ -265,7 +272,7 @@ public class SemanticChecker {
 
         boolean ok = true;
         Rule rule = new Rule();
 
         boolean ok = true;
         Rule rule = new Rule();
-        
+
         /* get rule type */
         boolean isstatic = pn.getChild("static") != null;
         boolean isdelay = pn.getChild("delay") != null;
         /* get rule type */
         boolean isstatic = pn.getChild("static") != null;
         boolean isdelay = pn.getChild("delay") != null;
@@ -276,11 +283,9 @@ public class SemanticChecker {
         assert sts.empty();
         sts.push(stGlobals);
         sts.push(rule.getSymbolTable());
         assert sts.empty();
         sts.push(stGlobals);
         sts.push(rule.getSymbolTable());
-
         /* optional quantifiers */
         if (pn.getChild("quantifiers") != null) {
             ParseNodeVector quantifiers = pn.getChild("quantifiers").getChildren();
         /* 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);
             for (int i = 0; i < quantifiers.size(); i++) {
                 ParseNode qn = quantifiers.elementAt(i);
                 Quantifier quantifier = parse_quantifier(qn);
@@ -290,9 +295,9 @@ public class SemanticChecker {
                 } else {
                     rule.addQuantifier(quantifier);
                 }
                 } else {
                     rule.addQuantifier(quantifier);
                 }
-            }             
+            }
         }
         }
-        
+
         /* get guard expr */
         Expr guard = parse_expr(pn.getChild("expr"));
 
         /* get guard expr */
         Expr guard = parse_expr(pn.getChild("expr"));
 
@@ -304,19 +309,19 @@ public class SemanticChecker {
 
         /* inclusion constraint */
         Inclusion inclusion = parse_inclusion(pn.getChild("inclusion"));
 
         /* inclusion constraint */
         Inclusion inclusion = parse_inclusion(pn.getChild("inclusion"));
-        
+
         if (inclusion == null) {
             ok = false;
         } else {
             rule.setInclusion(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. */
         /* 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 */
         assert sts.empty();
 
         /* add rule to global set */
@@ -333,7 +338,7 @@ public class SemanticChecker {
         if (pn.getChild("set") != null) {
             ParseNode set = pn.getChild("set");
             Expr expr = parse_expr(set.getChild("expr"));
         if (pn.getChild("set") != null) {
             ParseNode set = pn.getChild("set");
             Expr expr = parse_expr(set.getChild("expr"));
-            
+
             if (expr == null) {
                 return null;
             }
             if (expr == null) {
                 return null;
             }
@@ -341,7 +346,7 @@ public class SemanticChecker {
             String setname = set.getChild("name").getTerminal();
             assert setname != null;
             SetDescriptor sd = lookupSet(setname);
             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;
             if (sd == null) {
                 er.report(set.getChild("name"), "Undefined set '" + setname + "'");
                 return null;
@@ -352,7 +357,7 @@ public class SemanticChecker {
             ParseNode relation = pn.getChild("relation");
             Expr leftexpr = parse_expr(relation.getChild("left").getChild("expr"));
             Expr rightexpr = parse_expr(relation.getChild("right").getChild("expr"));
             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 ((leftexpr == null) || (rightexpr == null)) {
                 return null;
             }
@@ -376,10 +381,11 @@ public class SemanticChecker {
         if (!precheck(pn, "constraints")) {
             return false;
         }
         if (!precheck(pn, "constraints")) {
             return false;
         }
+        //System.out.println(pn.PPrint(2,true));
 
         boolean ok = true;
         ParseNodeVector constraints = pn.getChildren();
 
         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");
         for (int i = 0; i < constraints.size(); i++) {
             ParseNode constraint = constraints.elementAt(i);
             assert constraint.getLabel().equals("constraint");
@@ -390,6 +396,28 @@ public class SemanticChecker {
 
         /* do any post checks... (type constraints, etc?) */
 
 
         /* 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;
     }
 
        return ok;
     }
 
@@ -408,48 +436,50 @@ public class SemanticChecker {
         /* set up symbol table for constraint */
         assert sts.empty();
         sts.push(constraint.getSymbolTable());
         /* 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();
         /* 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) {
             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);
                 }
             }
         }
                     ok = false;
                 } else {
                     constraint.addQuantifier(quantifier);
                 }
             }
         }
-                                                      
+
         /* get body */
         LogicStatement logicexpr = parse_body(pn.getChild("body"));
 
         if (logicexpr == null) {
         /* 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);
         }
             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. */
         /* 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 */
         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 ok;
     }
 
     private Quantifier parse_quantifier(ParseNode pn) {
         if (!precheck(pn, "quantifier")) {
-            return null;           
+            return null;
         }
 
         if (pn.getChild("forall") != null) { /* forall element in Set */
         }
 
         if (pn.getChild("forall") != null) { /* forall element in Set */
@@ -457,10 +487,10 @@ public class SemanticChecker {
 
             /* get var */
             VarDescriptor vd = reserveName(pn.getChild("var"));
 
             /* get var */
             VarDescriptor vd = reserveName(pn.getChild("var"));
-            
+
             if (vd == null) {
                 return null;
             if (vd == null) {
                 return null;
-            } 
+            }
 
             sq.setVar(vd);
 
 
             sq.setVar(vd);
 
@@ -468,6 +498,7 @@ public class SemanticChecker {
             SetDescriptor set = parse_set(pn.getChild("set"));
             assert set != null;
             sq.setSet(set);
             SetDescriptor set = parse_set(pn.getChild("set"));
             assert set != null;
             sq.setSet(set);
+           vd.setSet(set);
 
             vd.setType(set.getType());
 
 
             vd.setType(set.getType());
 
@@ -480,13 +511,13 @@ public class SemanticChecker {
             /* get vars */
             VarDescriptor vd1 = reserveName(pn.getChild("left"));
             VarDescriptor vd2 = reserveName(pn.getChild("right"));
             /* get vars */
             VarDescriptor vd1 = reserveName(pn.getChild("left"));
             VarDescriptor vd2 = reserveName(pn.getChild("right"));
-            
+
             if ((vd1 == null) || (vd2 == null)) {
                 return null;
             }
             if ((vd1 == null) || (vd2 == null)) {
                 return null;
             }
-            
+
             rq.setTuple(vd1, vd2);
             rq.setTuple(vd1, vd2);
-            
+
             /* get relation */
             String relationname = pn.getChild("relation").getTerminal();
             assert relationname != null;
             /* get relation */
             String relationname = pn.getChild("relation").getTerminal();
             assert relationname != null;
@@ -495,14 +526,16 @@ public class SemanticChecker {
             if (rd == null) {
                 return null;
             }
             if (rd == null) {
                 return null;
             }
-            
+
             rq.setRelation(rd);
             vd1.setType(rd.getDomain().getType());
             rq.setRelation(rd);
             vd1.setType(rd.getDomain().getType());
+           vd1.setSet(rd.getDomain());
             vd2.setType(rd.getRange().getType());
             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();
             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"));
 
             /* grab var */
             VarDescriptor vd = reserveName(pn.getChild("var"));
 
@@ -510,6 +543,7 @@ public class SemanticChecker {
                 return null;
             }
 
                 return null;
             }
 
+           vd.setSet(lookupSet("int", false));
             vd.setType(ReservedTypeDescriptor.INT);
             fq.setVar(vd);
 
             vd.setType(ReservedTypeDescriptor.INT);
             fq.setVar(vd);
 
@@ -517,10 +551,11 @@ public class SemanticChecker {
             Expr lower = parse_expr(pn.getChild("lower").getChild("expr"));
             Expr upper = parse_expr(pn.getChild("upper").getChild("expr"));
 
             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;
             }
             if ((lower == null) || (upper == null)) {
                 return null;
             }
-
+           vd.setBounds(lower,upper);
             fq.setBounds(lower, upper);
 
             return fq;
             fq.setBounds(lower, upper);
 
             return fq;
@@ -531,19 +566,19 @@ public class SemanticChecker {
 
     private LogicStatement parse_body(ParseNode pn) {
         if (!precheck(pn, "body")) {
 
     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 (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;
             }
             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) {
             // 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) {
@@ -551,7 +586,7 @@ public class SemanticChecker {
             LogicStatement left, right;
             left = parse_body(pn.getChild("or").getChild("left").getChild("body"));
             right = parse_body(pn.getChild("or").getChild("right").getChild("body"));
             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;
             }
             if ((left == null) || (right == null)) {
                 return null;
             }
@@ -560,17 +595,16 @@ public class SemanticChecker {
         } else if (pn.getChild("not") != null) {
             /* NOT body */
             LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
         } else if (pn.getChild("not") != null) {
             /* NOT body */
             LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
-            
             if (left == null) {
                 return null;
             }
             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();
             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) {
     }
 
     private Predicate parse_predicate(ParseNode pn) {
@@ -580,11 +614,11 @@ public class SemanticChecker {
 
         if (pn.getChild("inclusion") != null) {
             ParseNode in = pn.getChild("inclusion");
 
         if (pn.getChild("inclusion") != null) {
             ParseNode in = pn.getChild("inclusion");
-            
+
             /* Expr */
             Expr expr = parse_expr(in.getChild("expr"));
             /* Expr */
             Expr expr = parse_expr(in.getChild("expr"));
-           
-            if (expr == null) { 
+
+            if (expr == null) {
                 return null;
             }
 
                 return null;
             }
 
@@ -598,7 +632,7 @@ public class SemanticChecker {
             return new InclusionPredicate(expr, setexpr);
         } else if (pn.getChild("expr") != null) {
             Expr expr = parse_expr(pn.getChild("expr"));
             return new InclusionPredicate(expr, setexpr);
         } else if (pn.getChild("expr") != null) {
             Expr expr = parse_expr(pn.getChild("expr"));
-            
+
             if (expr == null) {
                 return null;
             }
             if (expr == null) {
                 return null;
             }
@@ -606,18 +640,18 @@ public class SemanticChecker {
             return new ExprPredicate(expr);
         } else {
             throw new IRException();
             return new ExprPredicate(expr);
         } else {
             throw new IRException();
-        }       
+        }
     }
 
     private SetDescriptor parse_set(ParseNode pn) {
         if (!precheck(pn, "set")) {
             return null;
         }
     }
 
     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 (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");
             if (!stSets.contains(setname)) {
                 /* Semantic Error: unknown set */
                 er.report(pn, "Unknown set '" + setname + "' referenced in quantifier");
@@ -627,12 +661,12 @@ public class SemanticChecker {
                 SetDescriptor sd = (SetDescriptor) stSets.get(setname);
                 assert sd != null;
                 return sd;
                 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;
             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");
             for (int i = 0; i < token_literals.size(); i++) {
                 ParseNode literal = token_literals.elementAt(i);
                 assert literal.getLabel().equals("literal");
@@ -641,32 +675,32 @@ public class SemanticChecker {
                 if (litexpr == null) {
                     return null;
                 }
                 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 */
                 }
                 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());
         }
     }
 
             return tokenset;
         } else {
             throw new IRException(pn.getTerminal());
         }
     }
-    
+
     private boolean parse_space(ParseNode pn) {
         if (!precheck(pn, "space")) {
             return false;
         }
     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());
         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))) {
         /* parse sets */
         for (int i = 0; i < sets.size(); i++) {
             if (!parse_setdefinition(sets.elementAt(i))) {
@@ -685,17 +719,17 @@ public class SemanticChecker {
         // for cycles etc.
 
         // #TBD#: typecheck and check for cycles
         // for cycles etc.
 
         // #TBD#: typecheck and check for cycles
-      
+
         /* replace missing with actual */
         Iterator allsets = state.stSets.descriptors();
         /* 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);
         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());
 
                 if (subset instanceof MissingSetDescriptor) {
                     SetDescriptor newsubset = lookupSet(subset.getSymbol());
 
@@ -707,7 +741,7 @@ public class SemanticChecker {
                 }
             }
         }
                 }
             }
         }
-        
+
         return ok;
     }
 
         return ok;
     }
 
@@ -715,37 +749,37 @@ public class SemanticChecker {
         if (!precheck(pn, "setdefinition")) {
             return false;
         }
         if (!precheck(pn, "setdefinition")) {
             return false;
         }
-        
+
         boolean ok = true;
         boolean ok = true;
-        
+
         /* get set name */
         String setname = pn.getChild("name").getTerminal();
         assert (setname != null);
 
         SetDescriptor sd = new SetDescriptor(setname);
         /* 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 + "'");
         /* 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;
         } 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();
 
         /* 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));
             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 */
         }
 
         /* add set to symbol table */
@@ -786,14 +820,18 @@ public class SemanticChecker {
         assert rangesetname != null;
 
         /* get domain multiplicity */
         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 */
 
         /* 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. */
 
            set namespace is fully populated. any missing setdescriptors for the set
            symbol table will be assumed to be errors and reported. */
 
@@ -830,7 +868,7 @@ public class SemanticChecker {
         if (!precheck(pn, "structures")) {
             return false;
         }
         if (!precheck(pn, "structures")) {
             return false;
         }
-        
+
         boolean ok = true;
         ParseNodeVector structures = pn.getChildren("structure");
 
         boolean ok = true;
         ParseNodeVector structures = pn.getChildren("structure");
 
@@ -848,7 +886,7 @@ public class SemanticChecker {
             }
         }
 
             }
         }
 
-        // 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()) {
 
         Enumeration types = stTypes.getDescriptors();
         while (types.hasMoreElements()) {
@@ -857,9 +895,9 @@ public class SemanticChecker {
             if (t instanceof ReservedTypeDescriptor) {
                 // we don't need to check reserved types
             } else if (t instanceof StructureTypeDescriptor) {
             if (t instanceof ReservedTypeDescriptor) {
                 // we don't need to check reserved types
             } else if (t instanceof StructureTypeDescriptor) {
-                
+
                 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
                 StructureTypeDescriptor type = (StructureTypeDescriptor) t;
-                TypeDescriptor subtype = type.getSubType();
+                TypeDescriptor subtype = type.getSuperType();
 
                 // check that the subtype is valid
                 if (subtype instanceof MissingTypeDescriptor) {
 
                 // check that the subtype is valid
                 if (subtype instanceof MissingTypeDescriptor) {
@@ -870,14 +908,14 @@ public class SemanticChecker {
                         er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
                         ok = false;
                     } else {
                         er.report(null, "Undefined subtype '" + subtype.getSymbol() + "'");
                         ok = false;
                     } else {
-                        type.setSubType(newtype);
+                        type.setSuperType(newtype);
                     }
                 }
 
                 Iterator fields = type.getFields();
 
                 while (fields.hasNext()) {
                     }
                 }
 
                 Iterator fields = type.getFields();
 
                 while (fields.hasNext()) {
-                    FieldDescriptor field = (FieldDescriptor) fields.next();                        
+                    FieldDescriptor field = (FieldDescriptor) fields.next();
                     TypeDescriptor fieldtype = field.getType();
 
                     assert fieldtype != null;
                     TypeDescriptor fieldtype = field.getType();
 
                     assert fieldtype != null;
@@ -888,13 +926,17 @@ public class SemanticChecker {
                         if (newtype == null) {
                             // type never defined
                             // #TBD#: replace new ParseNode with original parsenode
                         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);
                         }
                         } else {
                             assert newtype != null;
                             field.setType(newtype);
                         }
-                    }                        
+                    }
                 }
 
                 Iterator labels = type.getLabels();
                 }
 
                 Iterator labels = type.getLabels();
@@ -919,7 +961,7 @@ public class SemanticChecker {
                         }
                     }
                 }
                         }
                     }
                 }
-                
+
             } else {
                 throw new IRException("shouldn't be any other typedescriptor classes");
             }
             } else {
                 throw new IRException("shouldn't be any other typedescriptor classes");
             }
@@ -937,13 +979,13 @@ public class SemanticChecker {
             if (t instanceof ReservedTypeDescriptor) {
                 // we don't need to check reserved types
             } else if (t instanceof StructureTypeDescriptor) {
             if (t instanceof ReservedTypeDescriptor) {
                 // we don't need to check reserved types
             } else if (t instanceof StructureTypeDescriptor) {
-                
+
                 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
                 StructureTypeDescriptor type = (StructureTypeDescriptor)t;
-                TypeDescriptor subtype = type.getSubType();
+                TypeDescriptor subtype = type.getSuperType();
                 Iterator fields = type.getFields();
 
                 while (fields.hasNext()) {
                 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;
 
                     if (field instanceof ArrayDescriptor) {
                         ArrayDescriptor ad = (ArrayDescriptor) field;
@@ -973,22 +1015,20 @@ public class SemanticChecker {
                                 public IRErrorReporter getErrorReporter() { return er; }
                                 public SymbolTable getSymbolTable() { return stGlobals; }
                             });
                                 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;
                         }
                     }
                 }
                         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");
             }
                 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
         }
 
         // #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;
         // cast, i believe
 
         return ok;
@@ -1004,17 +1044,17 @@ public class SemanticChecker {
 
         String type = pn.getChild("type").getTerminal();
         assert type != null;
 
         String type = pn.getChild("type").getTerminal();
         assert type != null;
+
         TypeDescriptor td = lookupType(type);
         assert td != 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 + "'");
             return false;
         }
 
         if (stGlobals.contains(name)) {
             /* redefinition of global */
             er.report(pn, "Redefinition of global '" + name + "'");
             return false;
         }
 
-        stGlobals.add(new VarDescriptor(name, name, td));
+        stGlobals.add(new VarDescriptor(name, name, td,true));
         return true;
     }
 
         return true;
     }
 
@@ -1026,7 +1066,7 @@ public class SemanticChecker {
         boolean ok = true;
         String typename = pn.getChild("name").getTerminal();
         StructureTypeDescriptor type = new StructureTypeDescriptor(typename);
         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();
         if (pn.getChild("subtype") != null) {
             // has a subtype, lets try to resolve it
             String subtype = pn.getChild("subtype").getTerminal();
@@ -1038,15 +1078,28 @@ public class SemanticChecker {
             }
 
             /* lookup the type to get the type descriptor */
             }
 
             /* lookup the type to get the type descriptor */
-            type.setSubType(lookupType(subtype, CREATE_MISSING));
+            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
         }
 
         // 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;
         dCurrentType = type;
-        
+
         // parse the labels and fields
         // parse the labels and fields
-        if (!parse_labelsandfields(pn.getChild("lf"))) {
+        if (pn.getChild("lf")!=null && !parse_labelsandfields(pn.getChild("lf"))) {
             ok = false;
         }
 
             ok = false;
         }
 
@@ -1056,7 +1109,7 @@ public class SemanticChecker {
         } else {
             stTypes.add(type);
         }
         } else {
             stTypes.add(type);
         }
-        
+
         return ok;
     }
 
         return ok;
     }
 
@@ -1066,8 +1119,8 @@ public class SemanticChecker {
         }
 
         boolean ok = true;
         }
 
         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;
         // to type check the labels)
         if (!parse_fields(pn.getChild("fields"))) {
             ok = false;
@@ -1085,17 +1138,17 @@ public class SemanticChecker {
         if (!precheck(pn, "fields")) {
             return false;
         }
         if (!precheck(pn, "fields")) {
             return false;
         }
-        
+
         boolean ok = true;
         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 */
         /* 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++) {
         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;
             FieldDescriptor fd;
             boolean reserved;
             String name = null;
@@ -1107,7 +1160,7 @@ public class SemanticChecker {
                 fd = new ReservedFieldDescriptor();
                 reserved = true;
             } else {
                 fd = new ReservedFieldDescriptor();
                 reserved = true;
             } else {
-                name = field.getChild("name").getTerminal();                
+                name = field.getChild("name").getTerminal();
                 fd = new FieldDescriptor(name);
                 reserved = false;
             }
                 fd = new FieldDescriptor(name);
                 reserved = false;
             }
@@ -1119,7 +1172,7 @@ public class SemanticChecker {
             fd.setType(lookupType(type, CREATE_MISSING));
 
             if (field.getChild("index") != null) {
             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"));
                 // field descriptor and then replace the top level field descriptor with
                 // this array descriptor
                 Expr expr = parse_expr(field.getChild("index").getChild("expr"));
@@ -1127,7 +1180,7 @@ public class SemanticChecker {
                     // #ATTN#: do we really want to return an exception here?
                     throw new IRException("invalid index expression");
                 }
                     // #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;
             }
 
                 fd = ad;
             }
 
@@ -1135,7 +1188,7 @@ public class SemanticChecker {
             if (reserved == false) {
                 // lets double check that we are redefining a field
                 if (dCurrentType.getField(name) != null) {
             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 {
                     er.report(pn, "Redefinition of field '" + name + "'");
                     ok = false;
                 } else {
@@ -1145,7 +1198,7 @@ public class SemanticChecker {
                 dCurrentType.addField(fd);
             }
         }
                 dCurrentType.addField(fd);
             }
         }
-        
+
         return ok;
     }
 
         return ok;
     }
 
@@ -1161,10 +1214,10 @@ public class SemanticChecker {
 
         ParseNodeVector labels = pn.getChildren();
 
 
         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();
             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"));
 
             if (label.getChild("index") != null) {
                 Expr expr = parse_expr(label.getChild("index").getChild("expr"));
@@ -1172,14 +1225,14 @@ public class SemanticChecker {
                     /* #ATTN#: do we really want to return an exception here? */
                     throw new IRException("Invalid expression");
                 }
                     /* #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 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) {
             FieldDescriptor fd = dCurrentType.getField(field);
 
             if (fd == null) {
@@ -1196,7 +1249,7 @@ public class SemanticChecker {
                 er.report(pn, "Redefinition of label '" + name + "'");
                 ok = false;
             } else {
                 er.report(pn, "Redefinition of label '" + name + "'");
                 ok = false;
             } else {
-                dCurrentType.addLabel(ld);            
+                dCurrentType.addLabel(ld);
             }
         }
 
             }
         }
 
@@ -1212,6 +1265,8 @@ public class SemanticChecker {
             // 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());
             // 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("literal") != null) {
             return parse_literal(pn.getChild("literal"));
         } else if (pn.getChild("operator") != null) {
@@ -1221,18 +1276,18 @@ public class SemanticChecker {
         } else if (pn.getChild("sizeof") != null) {
             return parse_sizeof(pn.getChild("sizeof"));
         } else if (pn.getChild("simple_expr") != 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) {
         } else if (pn.getChild("elementof") != null) {
-            return parse_elementof(pn.getChild("elementof"));        
+            return parse_elementof(pn.getChild("elementof"));
         } else if (pn.getChild("tupleof") != null) {
         } 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;
         } 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) {
     }
 
     private Expr parse_elementof(ParseNode pn) {
@@ -1252,7 +1307,7 @@ public class SemanticChecker {
 
         /* get left side expr */
         Expr expr = parse_expr(pn.getChild("expr"));
 
         /* get left side expr */
         Expr expr = parse_expr(pn.getChild("expr"));
-        
+
         if (expr == null) {
             return null;
         }
         if (expr == null) {
             return null;
         }
@@ -1264,7 +1319,7 @@ public class SemanticChecker {
         if (!precheck(pn, "tupleof")) {
             return null;
         }
         if (!precheck(pn, "tupleof")) {
             return null;
         }
-        
+
         /* get relation */
         String relname = pn.getChild("name").getTerminal();
         assert relname != null;
         /* get relation */
         String relname = pn.getChild("name").getTerminal();
         assert relname != null;
@@ -1318,23 +1373,23 @@ public class SemanticChecker {
 
         String relname = pn.getChild("name").getTerminal();
         boolean inverse = pn.getChild("inv") != 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;
         }
 
         if (expr == null) {
             return null;
         }
-                    
+
         RelationDescriptor relation = lookupRelation(relname);
         RelationDescriptor relation = lookupRelation(relname);
-            
+
         if (relation == null) {
             /* Semantic Error: relation not definied" */
             er.report(pn, "Undefined relation '" + relname + "'");
             return null;
         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);
 
         /* add usage so correct sets are created */
         relation.addUsage(inverse ? RelationDescriptor.INVIMAGE : RelationDescriptor.IMAGE);
-            
+
         return new RelationExpr(expr, relation, inverse);
     }
 
         return new RelationExpr(expr, relation, inverse);
     }
 
@@ -1345,7 +1400,7 @@ public class SemanticChecker {
 
         /* get setexpr */
         SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
 
         /* get setexpr */
         SetExpr setexpr = parse_setexpr(pn.getChild("setexpr"));
-        
+
         if (setexpr == null) {
             return null;
         }
         if (setexpr == null) {
             return null;
         }
@@ -1353,6 +1408,25 @@ public class SemanticChecker {
         return new SizeofExpr(setexpr);
     }
 
         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;
     private CastExpr parse_cast(ParseNode pn) {
         if (!precheck(pn, "cast")) {
             return null;
@@ -1367,14 +1441,14 @@ public class SemanticChecker {
             /* semantic error: undefined type in cast */
             er.report(pn, "Undefined type '" + typename + "' in cast operator");
             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"));
 
         /* get expr */
         Expr expr = parse_simple_expr(pn.getChild("simple_expr"));
-        
+
         if (expr == null) {
             return null;
         if (expr == null) {
             return null;
-        } 
+        }
 
         return new CastExpr(type, expr);
     }
 
         return new CastExpr(type, expr);
     }
@@ -1392,9 +1466,9 @@ public class SemanticChecker {
             SetDescriptor sd = lookupSet(setname);
 
             if (sd == null) {
             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;
                 return null;
-            } else {                         
+            } else {
                 return new SetExpr(sd);
             }
         } else if (pn.getChild("dot") != null) {
                 return new SetExpr(sd);
             }
         } else if (pn.getChild("dot") != null) {
@@ -1407,6 +1481,16 @@ public class SemanticChecker {
             RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
             relation.addUsage(RelationDescriptor.INVIMAGE);
             return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
             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();
         }
         } else {
             throw new IRException();
         }
@@ -1420,26 +1504,33 @@ public class SemanticChecker {
         /* get var */
         String varname = pn.getTerminal();
         assert varname != null;
         /* get var */
         String varname = pn.getTerminal();
         assert varname != null;
-        
+
         /* NOTE: quantifier var's are only found in the constraints and
         /* 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 */
            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)) {
 
         /* 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;
         }
     }
         } 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;
     private LiteralExpr parse_literal(ParseNode pn) {
         if (!precheck(pn, "literal")) {
             return null;
@@ -1450,8 +1541,8 @@ public class SemanticChecker {
                 return new BooleanLiteralExpr(true);
             } else {
                 return new BooleanLiteralExpr(false);
                 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 */
             String integer = pn.getChild("decimal").getTerminal();
 
             /* Check for integer literal overflow */
@@ -1485,7 +1576,7 @@ public class SemanticChecker {
 
     private OpExpr parse_operator(ParseNode pn) {
         if (!precheck(pn, "operator")) {
 
     private OpExpr parse_operator(ParseNode pn) {
         if (!precheck(pn, "operator")) {
-            return null; 
+            return null;
         }
 
         String opname = pn.getChild("op").getTerminal();
         }
 
         String opname = pn.getChild("op").getTerminal();
@@ -1495,15 +1586,15 @@ public class SemanticChecker {
             er.report(pn, "Unsupported operation: " + opname);
             return null;
         }
             er.report(pn, "Unsupported operation: " + opname);
             return null;
         }
-        
+
         Expr left = parse_expr(pn.getChild("left").getChild("expr"));
         Expr right = 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 (pn.getChild("right") != null) {
             right = parse_expr(pn.getChild("right").getChild("expr"));
         }
 
-        if (left == null) {           
+        if (left == null) {
             return null;
         }
 
             return null;
         }
 
@@ -1532,14 +1623,13 @@ public class SemanticChecker {
 
         if (pn.getChild("index") != null) {
             index = parse_expr(pn.getChild("index").getChild("expr"));
 
         if (pn.getChild("index") != null) {
             index = parse_expr(pn.getChild("index").getChild("expr"));
-            
+
             if (index == null) {
                 return null;
             }
         }
 
             if (index == null) {
                 return null;
             }
         }
 
-        return new DotExpr(left, field, index);        
+        return new DotExpr(left, field, index);
     }
 
 }
     }
 
 }
-
Data structure repair