Fixed lot of random bugs. Added code generate strings for expr's.

More code to generate concrete updates.  Initial code for computing
interference....

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index e87c1127f0778ed76d90ab4e4e58671900bb9f88..df39d0f2387cfd132224e7a36cd397cf8bf63520 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -68,7 +68,7 @@ public class Compiler {
                 FileOutputStream dotfile;
                 dotfile = new FileOutputStream(cli.infile + ".dependencies.edgelabels.dot");
                 GraphNode.useEdgeLabels = true;
-                GraphNode.DOTVisitor.visit(dotfile, nodes);                
+                GraphNode.DOTVisitor.visit(dotfile, nodes);
                 dotfile.close();
 
                 dotfile = new FileOutputStream(cli.infile + ".dependencies.dot");

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
index 037251a19670ef364cfb35fe0a7bdea1e79ca786..01cba236543a73499a3da1f91976c8fb07443209 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
@@ -10,6 +10,23 @@ class AbstractRepair {
     DNFPredicate torepair;
     int type;
     Descriptor descriptor;
+
+    public String type() {
+       switch(type) {
+       case ADDTOSET:
+           return "AddToSet";
+       case REMOVEFROMSET:
+           return "RemoveToSet";
+       case ADDTORELATION:
+           return "AddToRelation";
+       case REMOVEFROMRELATION:
+           return "RemoveFromRelation";
+       case MODIFYRELATION:
+           return "ModifyRelation";
+       default:
+           return "Unknown";
+       }
+    }
     
     public int getType() {
        return type;

diff --git a/Repair/RepairCompiler/MCC/IR/Binding.java b/Repair/RepairCompiler/MCC/IR/Binding.java
index 585107c79d95dd2961aeae45f71ed6e7240a6e90..652c849a16e12b564a9c43be1cbec6c5d23f2d4b 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Binding.java
+++ b/Repair/RepairCompiler/MCC/IR/Binding.java
@@ -3,16 +3,20 @@ package MCC.IR;
 class Binding {
     VarDescriptor var;
     int position;
-
+    boolean search;
     public Binding(VarDescriptor vd,int pos) {
        var=vd;
        position=pos;
+       search=false;
     }
 
+    public Binding(VarDescriptor vd) {
+       var=vd;
+       search=true;
+    }
     int getPosition() {
        return position;
     }
-
     VarDescriptor getVar() {
        return var;
     }

diff --git a/Repair/RepairCompiler/MCC/IR/BooleanLiteralExpr.java b/Repair/RepairCompiler/MCC/IR/BooleanLiteralExpr.java
index be7eb889ef9f6dbdeb35b351e77bb34e7ce360d7..727381825ab777eaaa69f57fceaf796399978ab8 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/BooleanLiteralExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/BooleanLiteralExpr.java
@@ -1,6 +1,7 @@
 package MCC.IR;
 
 import MCC.State;
+import java.util.Map;
 
 public class BooleanLiteralExpr extends LiteralExpr {
     
@@ -11,10 +12,20 @@ public class BooleanLiteralExpr extends LiteralExpr {
         td = ReservedTypeDescriptor.INT;
     }
 
-    public abstract boolean equals(Map remap, Expr e) {
+    public boolean usesDescriptor(Descriptor d) {
+       return false;
+    }
+
+    public String name() {
+       if (value)
+           return "true";
+       else return "false";
+    }
+
+    public boolean equals(Map remap, Expr e) {
        if (e==null)
            return false;
-       else if (!e instanceof BooleanLiteralExpr)
+       else if (!(e instanceof BooleanLiteralExpr))
            return false;
        else return (((BooleanLiteralExpr)e).value==value);
     }

diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java
index dc9c543c329412865f8a22d675aea5920d6d06ec..5b12c6dd95129b11c463e93010e2becbd6eaf582 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/CastExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java
@@ -12,12 +12,16 @@ public class CastExpr extends Expr {
         this.expr = expr;
     }
 
-    public abstract boolean equals(Map remap, Expr e) {
+    public boolean equals(Map remap, Expr e) {
        if (e==null)
            return false;
-       else if (!e instanceof CastExpr)
+       else if (!(e instanceof CastExpr))
            return false;
-       else return ((this.type==((CastExpr)e).type)&&equals(remap,expr,((CastExpr)e).expr));
+       else return ((this.type==((CastExpr)e).type)&&expr.equals(remap,((CastExpr)e).expr));
+    }
+
+    public boolean usesDescriptor(Descriptor d) {
+       return expr.usesDescriptor(d);
     }
 
     public Set getRequiredDescriptors() {

diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index e6718a69eefbf4f6b975b9cd1780709ff38a9328..aeaf4c91e7aa49061a7446c072de327c2e6bd712 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -6,14 +6,28 @@ class ConcreteInterferes {
            UpdateNode un=mun.getUpdate(i);
            for (int j=0;j<un.numUpdates();j++) {
                Updates update=un.getUpdate(j);
+               
                DNFRule drule=r.getDNFGuardExpr();
-               for(int k=0;k<drule.size();k++) {
-                   RuleConjunction rconj=drule.get(k);
-                   for(int l=0;l<rconj.size();l++) {
-                       DNFExpr dexpr=rconj.get(l);
-                       /* See if update interfers w/ dexpr */
-                       Descriptor updatedes=update.getDescriptor();
-                       
+               if (satisfy)
+                   drule=r.getDNFNegGuardExpr();
+
+               if (!update.isAbstract()) {
+                   Descriptor updated_des=update.getDescriptor();
+                   assert updated_des!=null;
+                   if (r.getInclusion().usesDescriptor(updated_des))
+                       return true; /* Interferes with inclusion condition */
+                   
+                   for(int k=0;k<drule.size();k++) {
+                       RuleConjunction rconj=drule.get(k);
+                       for(int l=0;l<rconj.size();l++) {
+                           DNFExpr dexpr=rconj.get(l);
+                           /* See if update interfers w/ dexpr */
+                           
+                           if (!dexpr.getExpr().usesDescriptor(updated_des))
+                               continue; /* No use of the descriptor */
+                           
+                           return true;
+                       }
                    }
                }
            }

diff --git a/Repair/RepairCompiler/MCC/IR/Conjunction.java b/Repair/RepairCompiler/MCC/IR/Conjunction.java
index 82e115f5c481c04822556702c85fe7ce0488db78..90e1f0904625211872e879fe5e74f82de14ff509 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Conjunction.java
+++ b/Repair/RepairCompiler/MCC/IR/Conjunction.java
@@ -11,7 +11,15 @@ public class Conjunction {
     Conjunction(Vector preds){
        predicates=preds       ;
     }
-
+    String name() {
+       String name="";
+       for(int i=0;i<predicates.size();i++) {
+           name+=((DNFPredicate)predicates.get(i)).name();
+           if (i!=(predicates.size()-1))
+               name+="&&";
+       }
+       return name;
+    }
     int size() {
        return predicates.size();
     }

diff --git a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
index 4aff0d5949a193636ac49a816e6446c6eeedef21..018df2fea7061c249748b6aaa86659cd8695ec05 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
@@ -6,7 +6,7 @@ public class DNFConstraint {
 
     public DNFConstraint(Predicate p) {
        conjunctions=new Vector();
-       conjunctions.add(new Conjunction(new DNFPredicate(true,p)));
+       conjunctions.add(new Conjunction(new DNFPredicate(false,p)));
     }
 
     public DNFConstraint(Conjunction conj) {

diff --git a/Repair/RepairCompiler/MCC/IR/DNFPredicate.java b/Repair/RepairCompiler/MCC/IR/DNFPredicate.java
index a1e5a65b45df55e3d71a4dc378f909d09cfb811b..cf7e16188507d55f6e954e437fa5b490e7b8b15e 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DNFPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFPredicate.java
@@ -15,6 +15,14 @@ public class DNFPredicate {
        this.negate=negate;
        this.predicate=predicate;
     }
+    String name() {
+       String name="";
+       if (this.negate)
+           name+="!";
+       name+=predicate.name();
+       return name;
+    }
+
     void negatePred() {
        negate=!negate;
     }

diff --git a/Repair/RepairCompiler/MCC/IR/DNFRule.java b/Repair/RepairCompiler/MCC/IR/DNFRule.java
index ab76f579f200aec5b304bb1626508242654300a1..345a588e788378d77577b9e2158fd9754398312f 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DNFRule.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFRule.java
@@ -6,7 +6,7 @@ public class DNFRule {
 
     public DNFRule(Expr e) {
        ruleconjunctions=new Vector();
-       ruleconjunctions.add(new RuleConjunction(new DNFExpr(true,e)));
+       ruleconjunctions.add(new RuleConjunction(new DNFExpr(false,e)));
     }
 
     public DNFRule(RuleConjunction conj) {

diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index 901b523d2b7730348490b26cd63b8c9c1e0c4d48..a380f4e6ea4ea68d1fbfaaab0fc1d544e203ca08 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -23,26 +23,41 @@ public class DotExpr extends Expr {
     FieldDescriptor fd;
     TypeDescriptor fieldtype;
     Expr intindex;
+
+    public String name() {
+       String name=left.name()+"."+field;
+       if (index!=null)
+           name+="["+index.name()+"]";
+       return name;
+    }
+    
+    public boolean usesDescriptor(Descriptor d) {
+       if (d==fd)
+           return true;
+       return left.usesDescriptor(d)||((intindex!=null)&&intindex.usesDescriptor(d));
+    }
+
+    public boolean equals(Map remap, Expr e) {
+       if (e==null||!(e instanceof DotExpr))
+           return false;
+       DotExpr de=(DotExpr)e;
+       if (!de.field.equals(field))
+           return false;
+       if (index==null) {
+           if (de.index!=null)
+               return false;
+       } else if (!index.equals(remap,de.index))
+           return false;
+       if (!left.equals(remap,de.left))
+           return false;
+       return true;
+    }
+
     
     public DotExpr(Expr left, String field, Expr index) {
         this.left = left;
         this.field = field;
         this.index = index;
-        StructureTypeDescriptor struct = (StructureTypeDescriptor) left.getType();        
-        FieldDescriptor fd = struct.getField(field);
-        LabelDescriptor ld = struct.getLabel(field);
-       if (ld != null) { /* label */
-            assert fd == null;
-            fieldtype = ld.getType(); // d.s ==> Superblock, while,  d.b ==> Block
-            fd = ld.getField();
-            assert fd != null;
-            assert intindex == null;
-            intindex = ld.getIndex();
-        } else {
-            fieldtype = fd.getType();
-           intindex=index;
-        }
-       this.fd=fd;
     }
 
     public Set getRequiredDescriptors() {
@@ -240,6 +255,25 @@ public class DotExpr extends Expr {
     public TypeDescriptor typecheck(SemanticAnalyzer sa) {
         TypeDescriptor lefttype = left.typecheck(sa);
         TypeDescriptor indextype = index == null ? null : index.typecheck(sa);
+       
+       {
+           /* finished typechecking...so we can fill the fields in */
+           StructureTypeDescriptor struct = (StructureTypeDescriptor) left.getType();        
+           FieldDescriptor fd = struct.getField(field);
+           LabelDescriptor ld = struct.getLabel(field);
+           if (ld != null) { /* label */
+               assert fd == null;
+               fieldtype = ld.getType(); // d.s ==> Superblock, while,  d.b ==> Block
+               fd = ld.getField();
+               assert fd != null;
+               assert intindex == null;
+               intindex = ld.getIndex();
+           } else {
+               fieldtype = fd.getType();
+               intindex=index;
+           }
+           this.fd=fd;
+       }
 
         if ((lefttype == null) || (index != null && indextype == null)) {
             return null;

diff --git a/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java b/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java
index 51941f90f2aa1a93a87528938f504d42cf51df66..1fdf42ad49778cf6ebf7d797f27a61f8b48e75fa 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java
@@ -11,10 +11,28 @@ public class ElementOfExpr extends Expr {
         if (element == null || set == null) {
             throw new NullPointerException();
         }
-
         this.element = element;
         this.set = set;
     }
+    public boolean usesDescriptor(Descriptor d) {
+       if (d==set)
+           return true;
+       return element.usesDescriptor(d);
+    }
+    public String name() {
+       return element.name()+" in "+set.toString();
+    }
+
+    public boolean equals(Map remap, Expr e) {
+       if (e==null||!(e instanceof ElementOfExpr))
+           return false;
+       ElementOfExpr eoe=(ElementOfExpr)e;
+       if (eoe.set!=set)
+           return false;
+       if (!element.equals(remap,eoe.element))
+           return false;
+       return true;
+    }
 
     public Set getRequiredDescriptors() {
         Set v = element.getRequiredDescriptors();

diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index 77ccbc630b44c46b305fa550207ef35207f36a13..4e9d283781c9b08b1b7e19fa28c38fd582335433 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -7,7 +7,7 @@ public abstract class Expr {
     TypeDescriptor td = null;
 
     public Expr() {}
-
+    /* Remap this's variables using the remap mapping */
     public abstract boolean equals(Map remap, Expr e);
 
     public abstract Set getRequiredDescriptors();
@@ -19,6 +19,10 @@ public abstract class Expr {
         return td;
     }
 
+    public String name() {
+       return "?";
+    }
+
     public abstract TypeDescriptor typecheck(SemanticAnalyzer sa);
 
     public abstract void prettyPrint(PrettyPrinter pp);
@@ -36,15 +40,17 @@ public abstract class Expr {
     }
 
     public int[] getRepairs(boolean negated) {
-       return new int[0];
+       System.out.println(this.getClass().getName());
+       throw new Error("Unrecognized EXPR");
     }
 
     public boolean inverted() {
        return false;
     }
 
-    public boolean usesDescriptor(RelationDescriptor rd) {
-       return false;
+    public boolean usesDescriptor(Descriptor rd) {
+       System.out.println(this.getClass().getName());
+       throw new Error("UNIMPLEMENTED");
     }
 
 }

diff --git a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
index 43ac5ad3ac0d3971bc9a1b179e7ff1a4b2ede44a..04b223ac205163fbdae870416e09c7cc7ed5eb64 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
@@ -10,6 +10,10 @@ public class ExprPredicate extends Predicate {
     public static final int SIZE=1;
     public static final int COMPARISON=2;
 
+    public String name() {
+       return expr.name();
+    }
+
     public int getType() {
        if (((OpExpr)expr).left instanceof SizeofExpr)
            return SIZE;

diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java
index 8059be37f278d4da4174da231aa4e7e87f8a1564..fde26adb66e41a3316c9665da51efaa27a0cdf7a 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphNode.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphNode.java
@@ -171,11 +171,11 @@ public class GraphNode {
         private void make() {
             output.println("digraph dotvisitor {");
             output.println("\trotate=90;");
-            output.println("\tpage=\"8.5,11\";");
-            output.println("\tnslimit=1000.0;");
-            output.println("\tnslimit1=1000.0;");
-            output.println("\tmclimit=1000.0;");
-            output.println("\tremincross=true;");
+           /*            output.println("\tpage=\"8.5,11\";");
+                         output.println("\tnslimit=1000.0;");
+                         output.println("\tnslimit1=1000.0;");
+                         output.println("\tmclimit=1000.0;");
+                         output.println("\tremincross=true;");*/
             output.println("\tnode [fontsize=10,height=\"0.1\", width=\"0.1\"];");
             output.println("\tedge [fontsize=6];");
 

diff --git a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
index 66437e3e9b82885b79468303ba8eeb80a6258b80..152a4f8277e02bdc715d5ef66e97e7e936a22a19 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
@@ -3,9 +3,7 @@ package MCC.IR;
 import java.util.*;
 
 public class ImageSetExpr extends SetExpr {
-    
-    public static final boolean INVERSE = true;
-
+    static final public boolean INVERSE=true;
     VarDescriptor vd;
     RelationDescriptor rd;
     boolean inverse;
@@ -16,12 +14,36 @@ public class ImageSetExpr extends SetExpr {
         this.inverse = false;
     }
 
+    public String name() {
+       String name=vd.toString()+".";
+       if (inverse)
+           name+="~";
+       name+=rd.toString();
+       return name;
+    }
+
     public ImageSetExpr(boolean inverse, VarDescriptor vd, RelationDescriptor rd) {
         this.vd = vd;
         this.rd = rd;
         this.inverse = inverse;
     }
 
+    public boolean equals(Map remap, Expr e) {
+       if (e==null||!(e instanceof ImageSetExpr))
+           return false;
+       ImageSetExpr ise=(ImageSetExpr)e;
+       if (ise.inverse!=inverse)
+           return false;
+       if (ise.rd!=rd)
+           return false;
+       VarDescriptor nvde=vd;
+       if (remap.containsKey(nvde))
+           nvde=(VarDescriptor)remap.get(nvde);
+       if (nvde!=ise.vd)
+           return false;
+       return true;
+    }
+
     public boolean inverted() {
        return inverse;
     }
@@ -38,8 +60,8 @@ public class ImageSetExpr extends SetExpr {
        return rd;
     }
 
-    public boolean usesDescriptor(RelationDescriptor rd) {
-       return (rd==this.rd);
+    public boolean usesDescriptor(Descriptor d) {
+       return (d==rd)||(d==vd);
     }
 
     public Set getInversedRelations() {

diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
index adea1ff758f7b569ae24dea2370b2565714a336b..8d619470d1ed42d8cfb6981be9f103f03341027c 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
+++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
@@ -24,8 +24,8 @@ public class ImplicitSchema {
            
            /* Construct quantifier */
            RelationQuantifier rq=new RelationQuantifier();
-           String varname1=new String("partitionvar1");
-           String varname2=new String("partitionvar2");
+           String varname1=new String("relationvar1");
+           String varname2=new String("relationvar2");
            VarDescriptor var1=new VarDescriptor(varname1);
            VarDescriptor var2=new VarDescriptor(varname2);
            c.getSymbolTable().add(var1);
@@ -35,11 +35,9 @@ public class ImplicitSchema {
            rq.setTuple(var1,var2);
            rq.setRelation(rd);
            c.addQuantifier(rq);
-
            VarExpr ve1=new VarExpr(varname1);
            SetExpr se1=new SetExpr(rd.getDomain());
            LogicStatement incpred1=new InclusionPredicate(ve1,se1);
-
            VarExpr ve2=new VarExpr(varname2);
            SetExpr se2=new SetExpr(rd.getRange());
            LogicStatement incpred2=new InclusionPredicate(ve2,se2);
@@ -54,7 +52,6 @@ public class ImplicitSchema {
            SetDescriptor sd=(SetDescriptor) setdescriptors.get(i);
            if(sd.isPartition()) {
                Constraint c=new Constraint();
-
                /* Construct quantifier */
                SetQuantifier sq=new SetQuantifier();
                String varname=new String("partitionvar");

diff --git a/Repair/RepairCompiler/MCC/IR/Inclusion.java b/Repair/RepairCompiler/MCC/IR/Inclusion.java
index 0fe01dae4339949ab2a8ff529faf70f688a531bb..8198b3f195535847802fcdecbc87348160c6596f 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Inclusion.java
+++ b/Repair/RepairCompiler/MCC/IR/Inclusion.java
@@ -13,6 +13,7 @@ public abstract class Inclusion {
     public abstract void generate(CodeWriter writer);
     
     public abstract boolean typecheck(SemanticAnalyzer sa);
+    public abstract boolean usesDescriptor(Descriptor d);
          
 }
 

diff --git a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
index e0d0d77ccbf4665b0c2f60dfcb77e42d49ad02e6..c27bb443333a892ea706e7df02a418671d873b5a 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
@@ -11,7 +11,10 @@ public class InclusionPredicate extends Predicate {
        return setexpr.inverted();
     }
 
-
+    public String name() {
+       return expr.name() + " in "+setexpr.name();
+    }
+    
     public InclusionPredicate(Expr expr, SetExpr setexpr) {
         if (expr == null) {
             throw new NullPointerException();

diff --git a/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java b/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java
index 49f52b581d04f9e554e9d9272022cb48f43fd655..e3f0d7347f5c62a6d9dfe19705421508049880c6 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java
@@ -1,18 +1,27 @@
 package MCC.IR;
+import java.util.Map;
 
 public class IntegerLiteralExpr extends LiteralExpr {
 
     int value;
 
+    public boolean usesDescriptor(Descriptor d) {
+       return false;
+    }
+
     public IntegerLiteralExpr(int value) {
         this.value = value; 
         td = ReservedTypeDescriptor.INT;
     }
 
-    public abstract boolean equals(Map remap, Expr e) {
+    public String name() {
+       return (new Integer(value)).toString();
+    }
+
+    public boolean equals(Map remap, Expr e) {
        if (e==null)
            return false;
-       else if (!e instanceof IntegerLiteralExpr)
+       else if (!(e instanceof IntegerLiteralExpr))
            return false;
        else return (((IntegerLiteralExpr)e).value==value);
     }

diff --git a/Repair/RepairCompiler/MCC/IR/LogicStatement.java b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
index 66674229b514081098bdceffe8e30072c7f4580f..aa093b4da76f4c2841488acf2abf9f753e05ad17 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/LogicStatement.java
+++ b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
@@ -8,6 +8,14 @@ public class LogicStatement {
     public static final Operation OR = new Operation("OR");
     public static final Operation NOT = new Operation("NOT");
 
+    public String name() {
+       String name=left.name();
+       name+=op.toString();
+       if (right!=null)
+           name+=right.name();
+       return name;
+    }
+
     public Set getInversedRelations() {
         if (left == null) {
             throw new IRException();

diff --git a/Repair/RepairCompiler/MCC/IR/MetaInclusion.java b/Repair/RepairCompiler/MCC/IR/MetaInclusion.java
index 52ab07873c68e7d1dd03ac65495fa3652ea7b132..3d00bbf726fbbcb7c47df1c642c5718720a8760e 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/MetaInclusion.java
+++ b/Repair/RepairCompiler/MCC/IR/MetaInclusion.java
@@ -14,6 +14,10 @@ public class MetaInclusion extends Inclusion {
         constraints = new Vector();
     }
 
+    public boolean usesDescriptor(Descriptor d) {
+       throw new Error("UNIMPLEMENTED");
+    }
+
     public Set getTargetDescriptors() {
         throw new IRException("unsupported");
     }

diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index b3af82790dede1e7479e376f8d0e9da86b5970ca..f903a337b504f3744d8437811ad605fe5559d149 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -16,10 +16,33 @@ public class OpExpr extends Expr {
         assert (right == null && opcode == Opcode.NOT) || (right != null);
     }
 
+    public String name() {
+       if (opcode==Opcode.NOT)
+           return "!("+left.name()+")";
+       String name=left.name()+opcode.toString();
+       if (right!=null)
+           name+=right.name();
+       return name;
+    }
+
     public Opcode getOpcode() {
        return opcode;
     }
 
+    public boolean equals(Map remap, Expr e) {
+       if (e==null||!(e instanceof OpExpr))
+           return false;
+       OpExpr oe=(OpExpr)e;
+       if (opcode!=oe.opcode)
+           return false;
+       if (!left.equals(remap,oe.left))
+           return false;
+       if (opcode!=Opcode.NOT)
+           if (!right.equals(remap,oe.right))
+               return false;
+       return true;
+    }
+
     public DNFRule constructDNF() {
         if (opcode==Opcode.AND) {
             DNFRule leftd=left.constructDNF();
@@ -35,12 +58,12 @@ public class OpExpr extends Expr {
         } else return new DNFRule(this);
     }
 
-    public boolean usesDescriptor(RelationDescriptor rd) {
+    public boolean usesDescriptor(Descriptor d) {
        if (opcode==Opcode.GT||opcode==Opcode.GE||opcode==Opcode.LT||
            opcode==Opcode.LE||opcode==Opcode.EQ||opcode==Opcode.NE)
-           return right.usesDescriptor(rd);
+           return right.usesDescriptor(d);
        else
-           return left.usesDescriptor(rd)||(right!=null&&right.usesDescriptor(rd));
+           return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
     }
     
     public int[] getRepairs(boolean negated) {

diff --git a/Repair/RepairCompiler/MCC/IR/RelationExpr.java b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
index fc2a4c7dabcc76494438fefd1e821e7c9b42b4bf..543b8e78cc4391088b5ada51dadd9fca1eb4f144 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RelationExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
@@ -14,11 +14,32 @@ public class RelationExpr extends Expr {
         this.inverse = inverse;
     }
 
+    public String name() {
+       String name=expr.name()+".";
+       if (inverse)
+           name+="~";
+       name+=relation.toString();
+       return name;
+    }
+
     public Expr getExpr() {
         return expr;
     }
 
-    public boolean usesDescriptor(RelationDescriptor rd) {
+    public boolean equals(Map remap, Expr e) {
+       if (e==null||!(e instanceof RelationExpr))
+           return false;
+       RelationExpr re=(RelationExpr)e;
+       if (re.relation!=relation)
+           return false;
+       if (!expr.equals(remap,re.expr))
+           return false;
+       if (inverse!=re.inverse)
+           return false;
+       return true;
+    }
+
+    public boolean usesDescriptor(Descriptor rd) {
        if (rd==relation)
            return true;
        else

diff --git a/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java b/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java
index cfbde5dfecdc6ebd6be47f47dd3f833570dde5db..f7e37cf0eea44a433c0073599cbc37d267716c6f 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java
@@ -17,6 +17,10 @@ public class RelationFunctionExpr extends Expr {
         this.rule = rule;
     }
 
+    public boolean equals(Map remap, Expr e) {
+       throw new Error("UNIMPLEMENTED!!!");
+    }
+
     public Descriptor getDescriptor() {
        return relation;
     }
@@ -35,7 +39,7 @@ public class RelationFunctionExpr extends Expr {
         return v;
     }
 
-    public boolean usesDescriptor(RelationDescriptor rd) {
+    public boolean usesDescriptor(Descriptor rd) {
        if (rd==relation)
            return true;
        else

diff --git a/Repair/RepairCompiler/MCC/IR/RelationInclusion.java b/Repair/RepairCompiler/MCC/IR/RelationInclusion.java
index ab6a8d40540a0bda5c369063bd198e63aa72e5e0..a2b40bcf00a213f757ce8c95685e61ab19436883 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RelationInclusion.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationInclusion.java
@@ -17,6 +17,14 @@ public class RelationInclusion extends Inclusion {
         this.relation = relation;
     }
 
+    public boolean usesDescriptor(Descriptor d) {
+       if (d==relation)
+           return true;
+       else
+           return(leftelementexpr.usesDescriptor(d)
+                  ||rightelementexpr.usesDescriptor(d));
+    }
+
     public Expr getLeftExpr() {
         return leftelementexpr;
     }

diff --git a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
index 265663cae46f27095017cdadf04187722c22dc6c..e94f7bd124a3fe7ed823df21d28209f6b8a96ee7 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
+++ b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
@@ -474,7 +474,7 @@ public class SemanticChecker {
             /* return to caller */
             return sq;
 
-        } else if (pn.getChild("relatiion") != null) { /* for < v1, v2 > in Relation */
+        } else if (pn.getChild("relation") != null) { /* for < v1, v2 > in Relation */
             RelationQuantifier rq = new RelationQuantifier();
 
             /* get vars */

diff --git a/Repair/RepairCompiler/MCC/IR/SetExpr.java b/Repair/RepairCompiler/MCC/IR/SetExpr.java
index b084b8e47bdba6143b83000a240b61931b225b55..d50c50ea393bfc0a39ccb2766a6a320e8a4a001d 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SetExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/SetExpr.java
@@ -9,7 +9,24 @@ public class SetExpr extends Expr {
     public SetExpr(SetDescriptor sd) {
         this.sd = sd;
     }
-    
+
+    public String name() {
+       return sd.toString();
+    }
+
+    public boolean equals(Map remap, Expr e) {
+       if (e==null||!(e instanceof SetExpr))
+           return false;
+       SetExpr se=(SetExpr)e;
+       if (sd!=se.sd)
+           return false;
+       return true;
+    }
+
+    public boolean usesDescriptor(Descriptor s) {
+       return (s==sd);
+    }
+
     public SetExpr() {
         this.sd = null;
     }

diff --git a/Repair/RepairCompiler/MCC/IR/SetInclusion.java b/Repair/RepairCompiler/MCC/IR/SetInclusion.java
index a9450d623a70f504ec25e0ef36b6f91e82046e24..cdf67b238585600140462842b981807bc39c46d8 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SetInclusion.java
+++ b/Repair/RepairCompiler/MCC/IR/SetInclusion.java
@@ -18,6 +18,13 @@ public class SetInclusion extends Inclusion {
         this.set = set;
     }
 
+    public boolean usesDescriptor(Descriptor d) {
+       if (d==set)
+           return true;
+       else
+           return elementexpr.usesDescriptor(d);
+    }
+
     public SetDescriptor getSet() {
         return set;
     }

diff --git a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
index 3d7f9acc5060c1bd4447ab9f360894dffd414647..7570ddc246bb5492c8dda34aab44183e4f71232b 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
@@ -14,7 +14,18 @@ public class SizeofExpr extends Expr {
         this.setexpr = setexpr;
     }
 
-    public boolean usesDescriptor(RelationDescriptor rd) {
+    public String name() {
+       return "size("+setexpr.name()+")";
+    }
+
+    public boolean equals(Map remap, Expr e) {
+       if (e==null||!(e instanceof SizeofExpr))
+           return false;
+       SizeofExpr soe=(SizeofExpr)e;
+       return setexpr.equals(remap,soe.setexpr);
+    }
+
+    public boolean usesDescriptor(Descriptor rd) {
        return setexpr.usesDescriptor(rd);
     }
 

diff --git a/Repair/RepairCompiler/MCC/IR/SizeofFunction.java b/Repair/RepairCompiler/MCC/IR/SizeofFunction.java
index 1342cfd02c8fe9c50db0b5e63c7413c6dae32186..45e63e7337cba76a958a3708de61d239e19b75e6 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SizeofFunction.java
+++ b/Repair/RepairCompiler/MCC/IR/SizeofFunction.java
@@ -18,6 +18,10 @@ public class SizeofFunction extends Expr {
         return new HashSet();
     }
 
+    public boolean equals(Map remap,Expr e) {
+       throw new Error("UNIMPLEMENTED");
+    }
+
     public Set getRequiredDescriptors() {
         // because we don't actually use rd for any generation, we return the empty set
         return new HashSet();

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 4d34f0054c8ebf2d5468e01ce56682695a23391f..0b01ab9a6db5071153e26041c366fa6c4242cd41 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -60,7 +60,9 @@ public class Termination {
            DNFConstraint dnf=c.dnfconstraint;
            for(int j=0;j<dnf.size();j++) {
                TermNode tn=new TermNode(c,dnf.get(j));
-               GraphNode gn=new GraphNode("Conjunction"+i+"B"+j,tn);
+               GraphNode gn=new GraphNode("Conj"+i+"A"+j,
+                                          "Conj ("+i+","+j+") "+dnf.get(j).name()
+                                          ,tn);
                conjunctions.add(gn);
                conjunctionmap.put(c,gn);
            }
@@ -165,7 +167,7 @@ public class Termination {
                for(int j=0;j<array.length;j++) {
                    AbstractRepair ar=new AbstractRepair(dp,array[j],d);
                    TermNode tn2=new TermNode(ar);
-                   GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+j,tn2);
+                   GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),tn2);
                    GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
                    gn.addEdge(e);
                    abstractrepair.add(gn2);
@@ -180,34 +182,72 @@ public class Termination {
            TermNode tn=(TermNode) gn.getOwner();
            AbstractRepair ar=tn.getAbstract();
            if (ar.getType()==AbstractRepair.ADDTOSET) {
-               generateaddtoset(gn,ar);
+               generateaddtosetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
-               generateremovefromset(gn,ar);
+               generateremovefromsetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
-               generateaddtorelation(gn,ar);
+               generateaddtosetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
-               generateremovefromrelation(gn,ar);
+               generateremovefromsetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
                generatemodifyrelation(gn,ar);
            }
        }
     }
 
-    void generateremovefromset(GraphNode gn,AbstractRepair ar) {
+    int removefromcount=0;
+    void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
        Vector possiblerules=new Vector();
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule) state.vRules.get(i);
            if ((r.getInclusion() instanceof SetInclusion)&&
                (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
                possiblerules.add(r);
+           if ((r.getInclusion() instanceof RelationInclusion)&&
+               (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
+               possiblerules.add(r);
        }
        int[] count=new int[possiblerules.size()];
        while(remains(count,possiblerules)) {
            MultUpdateNode mun=new MultUpdateNode(ar);
+           boolean goodflag=true;
            for(int i=0;i<possiblerules.size();i++) {
+               Rule r=(Rule)possiblerules.get(i);
                UpdateNode un=new UpdateNode();
+               /* Construct bindings */
+               Vector bindings=new Vector();
+               constructbindings(bindings, r,true);
+               if (count[i]<r.numQuantifiers()) {
+                   /* Remove quantifier */
+                   Quantifier q=r.getQuantifier(count[i]);
+                   if (q instanceof RelationQuantifier) {
+                       RelationQuantifier rq=(RelationQuantifier)q;
+                       TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
+                       toe.td=ReservedTypeDescriptor.INT;
+                       Updates u=new Updates(toe,true);
+                       un.addUpdate(u);
+                   } else if (q instanceof SetQuantifier) {
+                       SetQuantifier sq=(SetQuantifier)q;
+                       ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
+                       eoe.td=ReservedTypeDescriptor.INT;
+                       Updates u=new Updates(eoe,true);
+                       un.addUpdate(u);
+                   } else {goodflag=false;break;}
+               } else {
+                   int c=count[i]-r.numQuantifiers();
+                   if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
+                       goodflag=false;break;
+                   }
+               }
                mun.addUpdate(un);
-               /* CODE HERE*/
+           }
+           if (goodflag) {
+               TermNode tn=new TermNode(mun);
+               GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
+               GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
+               removefromcount++;
+               gn.addEdge(e);
+               updatenodes.add(gn2);
            }
            increment(count,possiblerules);
        }
@@ -232,164 +272,246 @@ public class Termination {
        return true;
     }
 
-    void generateremovefromrelation(GraphNode gn,AbstractRepair ar) {}
-    void generateaddtorelation(GraphNode gn,AbstractRepair ar) {}
-    void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {}
+    void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
+    }
+
+
+    boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
+       boolean goodupdate=true;
+       Inclusion inc=r.getInclusion();
+       for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
+           Quantifier q=(Quantifier)iterator.next();
+           if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
+               VarDescriptor vd=null;
+               SetDescriptor set=null;
+               if (q instanceof SetQuantifier) {
+                   vd=((SetQuantifier)q).getVar();
+               } else
+                   vd=((ForQuantifier)q).getVar();
+               if(inc instanceof SetInclusion) {
+                   SetInclusion si=(SetInclusion)inc;
+                   if ((si.elementexpr instanceof VarExpr)&&
+                       (((VarExpr)si.elementexpr).getVar()==vd)) {
+                       /* Can solve for v */
+                       Binding binding=new Binding(vd,0);
+                       bindings.add(binding);
+                   } else
+                       goodupdate=false;
+               } else if (inc instanceof RelationInclusion) {
+                   RelationInclusion ri=(RelationInclusion)inc;
+                   boolean f1=true;
+                   boolean f2=true;
+                   if ((ri.getLeftExpr() instanceof VarExpr)&&
+                       (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
+                               /* Can solve for v */
+                       Binding binding=new Binding(vd,0);
+                       bindings.add(binding);
+                   } else f1=false;
+                   if ((ri.getRightExpr() instanceof VarExpr)&&
+                       (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
+                               /* Can solve for v */
+                       Binding binding=new Binding(vd,0);
+                       bindings.add(binding);
+                   } else f2=false;
+                   if (!(f1||f2))
+                       goodupdate=false;
+               } else throw new Error("Inclusion not recognized");
+               if (!goodupdate)
+                   if (isremoval) {
+                       Binding binding=new Binding(vd);
+                       bindings.add(binding);
+                       goodupdate=true;
+                   } else
+                       break;
+           } else if (q instanceof RelationQuantifier) {
+               RelationQuantifier rq=(RelationQuantifier)q;
+               for(int k=0;k<2;k++) {
+                   VarDescriptor vd=(k==0)?rq.x:rq.y;
+                   if(inc instanceof SetInclusion) {
+                       SetInclusion si=(SetInclusion)inc;
+                       if ((si.elementexpr instanceof VarExpr)&&
+                           (((VarExpr)si.elementexpr).getVar()==vd)) {
+                           /* Can solve for v */
+                           Binding binding=new Binding(vd,0);
+                           bindings.add(binding);
+                       } else
+                           goodupdate=false;
+                   } else if (inc instanceof RelationInclusion) {
+                       RelationInclusion ri=(RelationInclusion)inc;
+                       boolean f1=true;
+                       boolean f2=true;
+                       if ((ri.getLeftExpr() instanceof VarExpr)&&
+                           (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
+                           /* Can solve for v */
+                           Binding binding=new Binding(vd,0);
+                           bindings.add(binding);
+                       } else f1=false;
+                       if ((ri.getRightExpr() instanceof VarExpr)&&
+                           (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
+                           /* Can solve for v */
+                           Binding binding=new Binding(vd,0);
+                           bindings.add(binding);
+                       } else f2=false;
+                       if (!(f1||f2))
+                           goodupdate=false;
+                   } else throw new Error("Inclusion not recognized");
+                   if (!goodupdate)
+                       if (isremoval) {
+                           Binding binding=new Binding(vd);
+                           bindings.add(binding);
+                           goodupdate=true;
+                       } else
+                           break;
+               }
+               if (!goodupdate)
+                   break;
+           } else throw new Error("Quantifier not recognized");
+       }
+       return goodupdate;
+    }
 
     static int addtocount=0;
-    void generateaddtoset(GraphNode gn, AbstractRepair ar) {
+    void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
+       System.out.println("Attempting to generate add to set");
+       System.out.println(ar.getPredicate().getPredicate().name());
+       System.out.println(ar.getPredicate().isNegated());
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule) state.vRules.get(i);
-           if (r.getInclusion() instanceof SetInclusion) {
-               if (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()) {
-                   //Generate add instruction
-                   DNFRule dnfrule=r.getDNFGuardExpr();
-                   for(int j=0;j<dnfrule.size();j++) {
-                       Inclusion inc=r.getInclusion();
-                       UpdateNode un=new UpdateNode();
-                       /* First solve for quantifiers */
-                       boolean goodupdate=true;
-                       for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
-                           Quantifier q=(Quantifier)iterator.next();
-                           boolean foundall=true;
-                           if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
-                               VarDescriptor vd=null;
-                               SetDescriptor set=null;
-                               if (q instanceof SetQuantifier) {
-                                   vd=((SetQuantifier)q).getVar();
-                               } else
-                                   vd=((ForQuantifier)q).getVar();
-                               if(inc instanceof SetInclusion) {
-                                   SetInclusion si=(SetInclusion)inc;
-                                   if ((si.elementexpr instanceof VarExpr)&&
-                                       (((VarExpr)si.elementexpr).getVar()==vd)) {
-                                       /* Can solve for v */
-                                       Binding binding=new Binding(vd,0);
-                                       un.addBinding(binding);
-                                   } else
-                                       foundall=false;
-                               } else if (inc instanceof RelationInclusion) {
-                                   RelationInclusion ri=(RelationInclusion)inc;
-                                   boolean f1=true;
-                                   boolean f2=true;
-                                   if ((ri.getLeftExpr() instanceof VarExpr)&&
-                                       (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
-                                       /* Can solve for v */
-                                       Binding binding=new Binding(vd,0);
-                                       un.addBinding(binding);
-                                   } else f1=false;
-                                   if ((ri.getRightExpr() instanceof VarExpr)&&
-                                       (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
-                                       /* Can solve for v */
-                                       Binding binding=new Binding(vd,0);
-                                       un.addBinding(binding);
-                                   } else f2=false;
-                                   if (!(f1||f2))
-                                       foundall=false;
-                               } else throw new Error("Inclusion not recognized");
-                           } else if (q instanceof RelationQuantifier) {
-                               RelationQuantifier rq=(RelationQuantifier)q;
-                               for(int k=0;k<2;k++) {
-                                   VarDescriptor vd=(k==0)?rq.x:rq.y;
-                                   if(inc instanceof SetInclusion) {
-                                       SetInclusion si=(SetInclusion)inc;
-                                       if ((si.elementexpr instanceof VarExpr)&&
-                                           (((VarExpr)si.elementexpr).getVar()==vd)) {
-                                           /* Can solve for v */
-                                           Binding binding=new Binding(vd,0);
-                                           un.addBinding(binding);
-                                       } else
-                                           foundall=false;
-                                   } else if (inc instanceof RelationInclusion) {
-                                       RelationInclusion ri=(RelationInclusion)inc;
-                                       boolean f1=true;
-                                       boolean f2=true;
-                                       if ((ri.getLeftExpr() instanceof VarExpr)&&
-                                           (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
-                                           /* Can solve for v */
-                                           Binding binding=new Binding(vd,0);
-                                           un.addBinding(binding);
-                                       } else f1=false;
-                                       if ((ri.getRightExpr() instanceof VarExpr)&&
-                                                  (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
-                                           /* Can solve for v */
-                                           Binding binding=new Binding(vd,0);
-                                           un.addBinding(binding);
-                                       } else f2=false;
-                                       if (!(f1||f2))
-                                           foundall=false;
-                                   } else throw new Error("Inclusion not recognized");
-                               }
-                           } else throw new Error("Quantifier not recognized");
-                           if (!foundall) {
-                               goodupdate=false;
-                               break;
+           /* See if this is a good rule*/
+           System.out.println(r.getGuardExpr().name());
+           if ((r.getInclusion() instanceof SetInclusion&&
+               ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
+               (r.getInclusion() instanceof RelationInclusion&&
+                ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
+
+               /* First solve for quantifiers */
+               Vector bindings=new Vector();
+               /* Construct bindings */
+               System.out.println("Attempting to generate add to set: #2");
+               if (!constructbindings(bindings,r,false))
+                   continue;
+               System.out.println("Attempting to generate add to set: #3");
+               //Generate add instruction
+               DNFRule dnfrule=r.getDNFGuardExpr();
+               for(int j=0;j<dnfrule.size();j++) {
+                   Inclusion inc=r.getInclusion();
+                   UpdateNode un=new UpdateNode();
+                   un.addBindings(bindings);
+                   /* Now build update for tuple/set inclusion condition */
+                   if(inc instanceof SetInclusion) {
+                       SetInclusion si=(SetInclusion)inc;
+                       if (!(si.elementexpr instanceof VarExpr)) {
+                           Updates up=new Updates(si.elementexpr,0);
+                           un.addUpdate(up);
+                       } else {
+                           VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
+                           if (un.getBinding(vd)==null) {
+                               Updates up=new Updates(si.elementexpr,0);
+                               un.addUpdate(up);
                            }
-                           /* Now build update for tuple/set inclusion condition */
-                           if(inc instanceof SetInclusion) {
-                               SetInclusion si=(SetInclusion)inc;
-                               if (!(si.elementexpr instanceof VarExpr)) {
-                                   Updates up=new Updates(si.elementexpr,0);
-                                   un.addUpdate(up);
-                               }
-                           } 
-                           if (inc instanceof RelationInclusion) {
-                               RelationInclusion ri=(RelationInclusion)inc;
-                               if (!(ri.getLeftExpr() instanceof VarExpr)) {
-                                   Updates up=new Updates(ri.getLeftExpr(),0);
-                                   un.addUpdate(up);
-                               }
-                               if (!(ri.getRightExpr() instanceof VarExpr)) {
-                                   Updates up=new Updates(ri.getRightExpr(),0);
-                                   un.addUpdate(up);
-                               }
+                       }
+                   } else if (inc instanceof RelationInclusion) {
+                       RelationInclusion ri=(RelationInclusion)inc;
+                       if (!(ri.getLeftExpr() instanceof VarExpr)) {
+                           Updates up=new Updates(ri.getLeftExpr(),0);
+                           un.addUpdate(up);
+                       } else {
+                           VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
+                           if (un.getBinding(vd)==null) {
+                               Updates up=new Updates(ri.getLeftExpr(),0);
+                               un.addUpdate(up);
                            }
-                           //Finally build necessary updates to satisfy conjunction
-                           RuleConjunction ruleconj=dnfrule.get(j);
-                           for(int k=0;k<ruleconj.size();k++) {
-                               DNFExpr de=ruleconj.get(k);
-                               Expr e=de.getExpr();
-                               if (e instanceof OpExpr) {
-                                   OpExpr ex=(OpExpr)de.getExpr();
-                                   Opcode op=ex.getOpcode();
-                                   if (de.getNegation()) {
-                                       /* remove negation through opcode translation */
-                                       if (op==Opcode.GT)
-                                           op=Opcode.LE;
-                                       else if (op==Opcode.GE)
-                                           op=Opcode.LT;
-                                       else if (op==Opcode.EQ)
-                                           op=Opcode.NE;
-                                       else if (op==Opcode.NE)
-                                           op=Opcode.EQ;
-                                       else if (op==Opcode.LT)
-                                           op=Opcode.GE;
-                                       else if (op==Opcode.LE)
-                                           op=Opcode.GT;
-                                   }
-                                   Updates up=new Updates(ex.left,ex.right,op);
-                                   un.addUpdate(up);
-                               } else if (e instanceof ElementOfExpr) {
-                                   Updates up=new Updates(e,de.getNegation());
-                                   un.addUpdate(up);
-                               } else if (e instanceof TupleOfExpr) {
-                                   Updates up=new Updates(e,de.getNegation());
-                                   un.addUpdate(up);
-                               } else throw new Error("Error #213");
+                       }
+                       if (!(ri.getRightExpr() instanceof VarExpr)) {
+                           Updates up=new Updates(ri.getRightExpr(),1);
+                           un.addUpdate(up);
+                       } else {
+                           VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
+                           if (un.getBinding(vd)==null) {
+                               Updates up=new Updates(ri.getRightExpr(),1);
+                               un.addUpdate(up);
                            }
                        }
+                   }
+                   //Finally build necessary updates to satisfy conjunction
+                   RuleConjunction ruleconj=dnfrule.get(j);
+                   /* Add in updates for quantifiers */
+                   System.out.println("Attempting to generate add to set #4");
+                   if (processquantifers(un, r)&&debugdd()&&
+                       processconjunction(un,ruleconj)) {
+                       System.out.println("Attempting to generate add to set #5");
                        MultUpdateNode mun=new MultUpdateNode(ar);
                        mun.addUpdate(un);
                        TermNode tn=new TermNode(mun);
-                       GraphNode gn2=new GraphNode("Update"+addtocount,tn);
+                       GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
                        GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
                        addtocount++;
                        gn.addEdge(e);
-                       updatenodes.add(gn2);
-                   }
+                       updatenodes.add(gn2);}
+               }
+           }
+       }
+    }
+
+    boolean debugdd() {
+       System.out.println("Attempting to generate add to set DD");
+       return true;
+    }
+
+    boolean processquantifers(UpdateNode un, Rule r) {
+       boolean goodupdate=true;
+       Inclusion inc=r.getInclusion();
+       for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
+           Quantifier q=(Quantifier)iterator.next();
+           /* Add quantifier */
+           /* FIXME: Analysis to determine when this update is necessary */
+           if (q instanceof RelationQuantifier) {
+               RelationQuantifier rq=(RelationQuantifier)q;
+               TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
+               toe.td=ReservedTypeDescriptor.INT;
+               Updates u=new Updates(toe,false);
+               un.addUpdate(u);
+           } else if (q instanceof SetQuantifier) {
+               SetQuantifier sq=(SetQuantifier)q;
+               ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
+               eoe.td=ReservedTypeDescriptor.INT;
+               Updates u=new Updates(eoe,false);
+               un.addUpdate(u);
+           } else {goodupdate=false; break;}
+       }
+       return goodupdate;
+    }
+
+    boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj){
+       boolean okay=true;
+       for(int k=0;k<ruleconj.size();k++) {
+           DNFExpr de=ruleconj.get(k);
+           Expr e=de.getExpr();
+           if (e instanceof OpExpr) {
+               OpExpr ex=(OpExpr)de.getExpr();
+               Opcode op=ex.getOpcode();
+               Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
+               un.addUpdate(up);
+           } else if (e instanceof ElementOfExpr) {
+               Updates up=new Updates(e,de.getNegation());
+               un.addUpdate(up);
+           } else if (e instanceof TupleOfExpr) {
+               Updates up=new Updates(e,de.getNegation());
+               un.addUpdate(up);
+           } else if (e instanceof BooleanLiteralExpr) { 
+               boolean truth=((BooleanLiteralExpr)e).getValue();
+               if (de.getNegation())
+                   truth=!truth;
+               if (!truth) {
+                   okay=false;
+                   break;
                }
+           } else {
+               System.out.println(e.getClass().getName());
+               throw new Error("Error #213");
            }
        }
+       return okay;
     }
 
     void generatescopenodes() {

diff --git a/Repair/RepairCompiler/MCC/IR/TokenLiteralExpr.java b/Repair/RepairCompiler/MCC/IR/TokenLiteralExpr.java
index 71b2ae07668584987af531da8ce8fa173424f3a4..9033ad205c0a5430e36d9082bb4a3aabd1215c7a 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/TokenLiteralExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/TokenLiteralExpr.java
@@ -22,12 +22,18 @@ public class TokenLiteralExpr extends LiteralExpr {
         }           
     }
 
-    public abstract boolean equals(Map remap, Expr e) {
-       if (e==null)
-           return false;
-       else if (!e instanceof TokenLiteralExpr)
+    public boolean usesDescriptor(Descriptor d) {
+       return false;
+    }
+
+    public String name() {
+       return token;
+    }
+
+    public boolean equals(Map remap, Expr e) {
+       if (e==null||!(e instanceof TokenLiteralExpr))
            return false;
-       else return ((BooleanLiteralExpr)e).num.equals(num);
+       else return ((TokenLiteralExpr)e).num.equals(num);
     }
 
     public String getValue() {

diff --git a/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java b/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java
index a726e044ba44901e497300782d9f6b2235075928..f0ccb85c428510d506ba3362597605a4f9874f3b 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java
@@ -18,6 +18,30 @@ public class TupleOfExpr extends Expr {
         this.relation = relation;
     }
 
+    public String name() {
+       return "<"+left.name()+","+right.name()+"> in "+relation.toString();
+    }
+
+    public boolean usesDescriptor(Descriptor d) {
+       if (d==relation)
+           return true;
+       else
+           return left.usesDescriptor(d)||right.usesDescriptor(d);
+    }
+
+    public boolean equals(Map remap, Expr e) {
+       if (e==null||!(e instanceof TupleOfExpr))
+           return false;
+       TupleOfExpr toe=(TupleOfExpr)e;
+       if (!left.equals(remap,toe.left))
+           return false;
+       if (!right.equals(remap,toe.right))
+           return false;
+       if (relation!=toe.relation)
+           return false;
+       return true;
+    }
+
     public Set getRequiredDescriptors() {
         Set v = left.getRequiredDescriptors();
         v.addAll(right.getRequiredDescriptors());

diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
index 3a02c3792d0c5bba0931389bee2804d6b979b1dc..31e954c03c053ca3764d979346fb627fb3075326 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/UpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -4,16 +4,33 @@ import java.util.*;
 class UpdateNode {
     Vector updates;
     Vector bindings;
+    Hashtable binding;
 
     public UpdateNode() {
        updates=new Vector();
        bindings=new Vector();
+       binding=new Hashtable();
+    }
+
+    public void addBindings(Vector v) {
+       for (int i=0;i<v.size();i++) {
+           bindings.add((Binding)v.get(i));
+       }
     }
 
     public void addBinding(Binding b) {
        bindings.add(b);
+       binding.put(b.getVar(),b);
     }
 
+    public Binding getBinding(VarDescriptor vd) {
+       if (binding.containsKey(vd))
+           return (Binding)binding.get(vd);
+       else
+           return null;
+    }
+
+
     public void addUpdate(Updates u) {
        updates.add(u);
     }

diff --git a/Repair/RepairCompiler/MCC/IR/Updates.java b/Repair/RepairCompiler/MCC/IR/Updates.java
index 3f99fe215b0b633d0e19054d6d2a71d0e3afdd72..e0492d426b976d06a22fb6dba17b1bbb4e04cd91 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Updates.java
+++ b/Repair/RepairCompiler/MCC/IR/Updates.java
@@ -11,9 +11,37 @@ class Updates {
     Opcode opcode;
     boolean negate;
 
-    public Updates(Expr lexpr, Expr rexpr, Opcode op) {
+    public String toString() {
+       String st="type="+type+"\n";
+       st+="rightposition="+rightposition+"\n";
+       if (rightexpr!=null)
+           st+="rightexpr="+rightexpr.name()+"\n";
+       if (leftexpr!=null)
+           st+="leftexpr="+leftexpr.name()+"\n";
+       st+="opcode="+opcode+"\n";
+       st+="negate="+negate+"\n";
+       return st;
+    }
+
+    public Updates(Expr lexpr, Expr rexpr, Opcode op, boolean negate) {
        leftexpr=lexpr;
        type=Updates.EXPR;
+       if (negate) {
+       /* remove negation through opcode translation */
+           if (op==Opcode.GT)
+               op=Opcode.LE;
+           else if (op==Opcode.GE)
+               op=Opcode.LT;
+           else if (op==Opcode.EQ)
+               op=Opcode.NE;
+           else if (op==Opcode.NE)
+               op=Opcode.EQ;
+           else if (op==Opcode.LT)
+               op=Opcode.GE;
+           else if (op==Opcode.LE)
+               op=Opcode.GT;
+       }
+
        opcode=Opcode.EQ;
        /* Get rid of everything but NE */
        if (op==Opcode.GT) {
@@ -37,12 +65,17 @@ class Updates {
        else return false;
     }
 
+
+
     Descriptor getDescriptor() {
        if (isGlobal()) {
            return ((VarExpr)leftexpr).getVar();
        } else if (isField()) {
            return ((DotExpr)leftexpr).getField();
-       } else throw new Error("Unrecognized Update");
+       } else {
+           System.out.println(toString());
+           throw new Error("Unrecognized Update");
+       }
     }
 
     boolean isField() {
@@ -71,6 +104,11 @@ class Updates {
        type=Updates.POSITION;
        opcode=null;
     }
+
+    boolean isAbstract() {
+       return type==Updates.ABSTRACT;
+    }
+
     public Updates(Expr lexpr,boolean negates) {
        leftexpr=lexpr;
        type=Updates.ABSTRACT;

diff --git a/Repair/RepairCompiler/MCC/IR/VarExpr.java b/Repair/RepairCompiler/MCC/IR/VarExpr.java
index a697a5fa9a0eb5ba885db9f71ac83eebc3c19063..82cd3419806f3b84028778b2e715ac77e1ea81d2 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/VarExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/VarExpr.java
@@ -12,6 +12,38 @@ public class VarExpr extends Expr {
         this.varname = varname; 
     }
 
+    public VarExpr(VarDescriptor vd) {
+       this.vd=vd;
+       varname=vd.getSymbol();
+        this.td = vd.getType();        
+    }
+
+    public String name() {
+       return varname;
+    }
+
+    public boolean usesDescriptor(Descriptor d) {
+       if (d==vd)
+           return true;
+       return false;
+    }
+
+    public boolean equals(Map remap, Expr e) {
+       if (e==null||!(e instanceof VarExpr))
+           return false;
+       VarExpr ve=(VarExpr)e;
+       if (vd==null)
+           throw new Error("Uninitialized VarDescriptor");
+       if (ve.vd==null)
+           throw new Error("e has uninitialized VarDescriptor");
+       VarDescriptor nvd=vd;
+       if (remap.containsKey(nvd))
+           nvd=(VarDescriptor)remap.get(nvd);
+       if (nvd!=ve.vd)
+           return false;
+       return true;
+    }
+
     public Set getInversedRelations() {
         return new HashSet();
     }

diff --git a/Repair/RepairCompiler/MCC/link.model b/Repair/RepairCompiler/MCC/link.model
index 855104cb07fdc9149cac1e43aecad3b5e9a73c72..18c9466026c49b1727f5e798fa312f4c8ac43da4 100755 (executable)
--- a/Repair/RepairCompiler/MCC/link.model
+++ b/Repair/RepairCompiler/MCC/link.model
@@ -1,7 +1,7 @@
 [], literal(true) => head in Nodes;
-[forall node in Nodes], !node.next=literal(0) => node.next in Nodes;
-[forall node in Nodes], !node.next=literal(0) => <node, node.next> in nextnodes;
-[forall node in Nodes], !node.prev=literal(0) => node.prev in Nodes;
-[forall node in Nodes], !node.prev=literal(0) => <node, node.prev> in prevnodes;
+[forall node in Nodes], !(node.next=literal(0)) => node.next in Nodes;
+[forall node in Nodes], !(node.next=literal(0)) => <node, node.next> in nextnodes;
+[forall node in Nodes], !(node.prev=literal(0)) => node.prev in Nodes;
+[forall node in Nodes], !(node.prev=literal(0)) => <node, node.prev> in prevnodes;