From: bdemsky <bdemsky>
Date: Wed, 27 Oct 2004 19:04:55 +0000 (+0000)
Subject: Adding support for sum expressions.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=commitdiff_plain;h=8599e7b56823377d9757eb7e5319a53c7073314a

Adding support for sum expressions.
---

diff --git a/Repair/RepairCompiler/MCC/CDL.cup b/Repair/RepairCompiler/MCC/CDL.cup
index 12021e6..f491a6e 100755
--- a/Repair/RepairCompiler/MCC/CDL.cup
+++ b/Repair/RepairCompiler/MCC/CDL.cup
@@ -132,6 +132,7 @@ parser code {:
     terminal SUB; 
     terminal MULT; 
     terminal DIV;
+    terminal SUM;
 
     terminal NOT;
     terminal LT;
@@ -141,7 +142,6 @@ parser code {:
     terminal EQ;
     terminal NE;
 
-
     terminal FORALL;
     terminal IN;
     terminal INTEST;
@@ -478,8 +478,17 @@ setexpr ::=
 	;
 	
 expr ::=
-	
-	ID:var
+
+	SUM OPENPAREN ID:set DOT ID:relation CLOSEPAREN
+	{:
+	debugMessage(PRODSTRING);
+	ParseNode expr = new ParseNode("sumexpr", parser.curLine(3));
+	expr.addChild("dot").addChild("set", parser.curLine(3)).addChild(set);
+	expr.getChild("dot").addChild("relation", parser.curLine(1)).addChild(relation);
+	RESULT = expr;
+	:}
+
+	| ID:var
 	{:
 	debugMessage(PRODSTRING);
      	ParseNode expr = new ParseNode("expr", parser.curLine(1));	
diff --git a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
index 2e54c87..734f6d0 100755
--- a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
+++ b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
@@ -1265,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());
+        } 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) {
@@ -1406,6 +1408,25 @@ public class SemanticChecker {
         return new SizeofExpr(setexpr);
     }
 
+    private SumExpr parse_sum(ParseNode pn) {
+        if (!precheck(pn, "sumexpr")) {
+            return null;
+        }
+        String setname = pn.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;
diff --git a/Repair/RepairCompiler/MCC/IR/SumExpr.java b/Repair/RepairCompiler/MCC/IR/SumExpr.java
new file mode 100755
index 0000000..a03338e
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/SumExpr.java
@@ -0,0 +1,77 @@
+package MCC.IR;
+
+import java.util.*;
+
+public class SumExpr extends Expr {
+
+    SetDescriptor sd;
+    RelationDescriptor rd;
+
+
+    public SumExpr(SetDescriptor sd, RelationDescriptor rd) {
+        if (sd == null||rd==null) {
+            throw new NullPointerException();
+        }
+        this.sd=sd;
+        this.rd=rd;
+    }
+
+    public String name() {
+	return "sum("+sd.getSafeSymbol()+"."+rd.getSafeSymbol()+")";
+    }
+
+    public boolean equals(Map remap, Expr e) {
+	if (e==null||!(e instanceof SumExpr))
+	    return false;
+	SumExpr se=(SumExpr)e;
+	return (se.sd==sd)&&(se.rd==rd);
+    }
+
+    public boolean usesDescriptor(Descriptor d) {
+        return (sd==d)||(rd==d);
+    }
+
+    public Set useDescriptor(Descriptor d) {
+        HashSet newset=new HashSet();
+        if ((d==sd)||(d==rd))
+            newset.add(this);
+        return newset;
+    }
+
+    public Descriptor getDescriptor() {
+        throw new Error();
+    }
+
+    public boolean inverted() {
+	return false;
+    }
+
+    public Set getRequiredDescriptors() {
+        HashSet v=new HashSet();
+        v.add(sd);
+        v.add(rd);
+        return v;
+    }
+
+    public void generate(CodeWriter writer, VarDescriptor dest) {
+        throw new Error();
+    }
+
+    public void prettyPrint(PrettyPrinter pp) {
+        pp.output("sum(");
+        pp.output(sd.getSafeSymbol());
+        pp.output(".");
+        pp.output(rd.getSafeSymbol());
+        pp.output(")");
+    }
+
+    public TypeDescriptor typecheck(SemanticAnalyzer sa) {
+        this.td = ReservedTypeDescriptor.INT;
+        return this.td;
+    }
+
+    public Set getInversedRelations() {
+        return new HashSet();
+    }
+
+}
diff --git a/Repair/RepairCompiler/MCC/Lexer.lex b/Repair/RepairCompiler/MCC/Lexer.lex
index ed6f239..0664e0b 100755
--- a/Repair/RepairCompiler/MCC/Lexer.lex
+++ b/Repair/RepairCompiler/MCC/Lexer.lex
@@ -29,19 +29,20 @@ CHAR=(\\\"|\\\'|\\\\|\\t|\\n|[\x20-\x21\x23-\x26\x28-\x5B\x5D-\x7E])
 %%
 
 <YYINITIAL> {WHITESPACE}		{}
-<YYINITIAL> \n				{ LineCount.addLineBreak(yychar+1); } 
+<YYINITIAL> \n				{ LineCount.addLineBreak(yychar+1); }
 
-<YYINITIAL> "{"				{ return tok(Sym.OPENBRACE, yytext()); } 
-<YYINITIAL> "}"				{ return tok(Sym.CLOSEBRACE, yytext()); } 
-<YYINITIAL> "("				{ return tok(Sym.OPENPAREN, yytext()); } 
-<YYINITIAL> ")"				{ return tok(Sym.CLOSEPAREN, yytext()); } 
-<YYINITIAL> "["				{ return tok(Sym.OPENBRACKET, yytext()); } 
-<YYINITIAL> "]"				{ return tok(Sym.CLOSEBRACKET, yytext()); } 
+<YYINITIAL> "{"				{ return tok(Sym.OPENBRACE, yytext()); }
+<YYINITIAL> "}"				{ return tok(Sym.CLOSEBRACE, yytext()); }
+<YYINITIAL> "("				{ return tok(Sym.OPENPAREN, yytext()); }
+<YYINITIAL> ")"				{ return tok(Sym.CLOSEPAREN, yytext()); }
+<YYINITIAL> "["				{ return tok(Sym.OPENBRACKET, yytext()); }
+<YYINITIAL> "]"				{ return tok(Sym.CLOSEBRACKET, yytext()); }
 
 <YYINITIAL> "+"				{ return tok(Sym.ADD, yytext()); }
 <YYINITIAL> "-"				{ return tok(Sym.SUB, yytext()); }
 <YYINITIAL> "*"				{ return tok(Sym.MULT, yytext()); }
 <YYINITIAL> "/"				{ return tok(Sym.DIV, yytext()); }
+<YYINITIAL> sum			        { return tok(Sym.SUM, yytext()); }
 
 
 <YYINITIAL> "<"				{ return tok(Sym.LT, yytext()); }
@@ -56,11 +57,11 @@ CHAR=(\\\"|\\\'|\\\\|\\t|\\n|[\x20-\x21\x23-\x26\x28-\x5B\x5D-\x7E])
 <YYINITIAL> in\?                        { return tok(Sym.INTEST, yytext()); }
 <YYINITIAL> in                          { return tok(Sym.IN, yytext()); }
 
-<YYINITIAL> ","				{ return tok(Sym.COMMA, yytext()); } 
+<YYINITIAL> ","				{ return tok(Sym.COMMA, yytext()); }
 <YYINITIAL> sizeof                      { return tok(Sym.SIZEOF, yytext()); }
 
-<YYINITIAL> ".~"			{ return tok(Sym.DOTINV, yytext()); } 
-<YYINITIAL> "."				{ return tok(Sym.DOT, yytext()); } 
+<YYINITIAL> ".~"			{ return tok(Sym.DOTINV, yytext()); }
+<YYINITIAL> "."				{ return tok(Sym.DOT, yytext()); }
 
 <YYINITIAL> "and"			{ return tok(Sym.AND, yytext()); }
 <YYINITIAL> "or" 			{ return tok(Sym.OR, yytext()); }
diff --git a/Repair/RepairCompiler/MCC/MDL.cup b/Repair/RepairCompiler/MCC/MDL.cup
index c25e436..0ba43a7 100755
--- a/Repair/RepairCompiler/MCC/MDL.cup
+++ b/Repair/RepairCompiler/MCC/MDL.cup
@@ -139,6 +139,7 @@ parser code {:
     terminal SUB; 
     terminal MULT; 
     terminal DIV;
+    terminal SUM;
 
     terminal NOT;
     terminal LT;
diff --git a/Repair/RepairCompiler/MCC/SDL.cup b/Repair/RepairCompiler/MCC/SDL.cup
index be328fe..4547171 100755
--- a/Repair/RepairCompiler/MCC/SDL.cup
+++ b/Repair/RepairCompiler/MCC/SDL.cup
@@ -122,6 +122,7 @@ parser code {:
     terminal SUB; 
     terminal MULT; 
     terminal DIV;
+    terminal SUM;
 
     terminal NOT;
     terminal LT;
diff --git a/Repair/RepairCompiler/MCC/TDL.cup b/Repair/RepairCompiler/MCC/TDL.cup
index ee4ba59..c905958 100755
--- a/Repair/RepairCompiler/MCC/TDL.cup
+++ b/Repair/RepairCompiler/MCC/TDL.cup
@@ -120,6 +120,7 @@ parser code {:
     terminal SUB; 
     terminal MULT; 
     terminal DIV;
+    terminal SUM;
 
     terminal NOT;
     terminal LT;