1) Added useDescriptor method to Expr's.

2) Generalized analysis to determine that an update effecting a rule won't change other bindings of the same rule...

diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java
index 44e085d77d9134f4fde113df0591c554a8cfe4eb..d36aabbd4496da5ce7288f31909f429801f282e8 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/CastExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java
@@ -38,6 +38,10 @@ public class CastExpr extends Expr {
        else return ((this.type==((CastExpr)e).type)&&expr.equals(remap,((CastExpr)e).expr));
     }
 
+    public Set useDescriptor(Descriptor d) {
+       return expr.useDescriptor(d);
+    }
+
     public boolean usesDescriptor(Descriptor d) {
        return expr.usesDescriptor(d);
     }

diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index f8d82d522eef4d5bf0b42cce1e6fd3ae073e68ac..af193f7ec4dc7df0ab1d396633a7ef8249ff7e5f 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -1,7 +1,13 @@
 package MCC.IR;
 import java.util.*;
 
-class ConcreteInterferes {
+public class ConcreteInterferes {
+    Termination termination;
+
+    public ConcreteInterferes(Termination t) {
+       this.termination=t;
+    }
+
 
     static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
        Descriptor updated_des=update.getDescriptor();
@@ -148,7 +154,7 @@ class ConcreteInterferes {
     /** Returns true if the data structure updates performed by mun may increase (or decrease if satisfy=false)
      * the scope of the model definition rule r. */
 
-    static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+    public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
        if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
            return false;
        for(int i=0;i<mun.numUpdates();i++) {
@@ -169,36 +175,45 @@ class ConcreteInterferes {
                       If we're removing something, there is no similar side effect */
 
                    /* ISSUE: Rules need to be updated if we allow concrete expression of the form x.f.g */
-                   if ((un.getRule()==r)&&
-                       (((mun.op==MultUpdateNode.ADD)&&satisfy)||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)||(mun.op==MultUpdateNode.MODIFY))&&
-                       (r.numQuantifiers()==1)&&
-                       (r.getQuantifier(0) instanceof SetQuantifier)&&
-                       update.isField()&&
-                       (((DotExpr)update.getLeftExpr()).getExpr() instanceof VarExpr)&&
-                       ((SetQuantifier)r.getQuantifier(0)).getVar()==((VarExpr)((DotExpr)update.getLeftExpr()).getExpr()).getVar())
-                       continue;
-
-                   if ((un.getRule()==r)&&
-                       (((mun.op==MultUpdateNode.ADD)&&satisfy)||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)||(mun.op==MultUpdateNode.MODIFY))&&
-                       (r.numQuantifiers()==0))
-                       continue;
-                   
-
                    if (r.getInclusion().usesDescriptor(updated_des)) {
-                       if (satisfy) {
-                           if (interferesinclusion(un, update, r))
-                           return true;
-                       } else
-                           return true; /* Interferes with inclusion condition */
+                       boolean ok=false;
+                       if ((un.getRule()==r)&&
+                           (((mun.op==MultUpdateNode.ADD)&&satisfy)
+                            ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
+                            ||(mun.op==MultUpdateNode.MODIFY))) {
+                           Inclusion inclusion=r.getInclusion();
+                           if (inclusion instanceof RelationInclusion) {
+                               RelationInclusion ri=(RelationInclusion)inclusion;
+                               if ((!interferes(update,r,ri.getLeftExpr()))&&
+                                   (!interferes(update,r,ri.getRightExpr())))
+                                   ok=true;
+                           } else if (inclusion instanceof SetInclusion) {
+                               SetInclusion si=(SetInclusion)inclusion;
+                               if (!interferes(update,r,si.getExpr()))
+                                   ok=true;
+                           } else throw new Error();
+                       }
+                       if (!ok) {
+                           if (satisfy) {
+                               if (interferesinclusion(un, update, r))
+                                   return true;
+                           } else
+                               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 interferes w/ dexpr */
+                           if ((un.getRule()==r)&&
+                               (((mun.op==MultUpdateNode.ADD)&&satisfy)
+                                ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
+                                ||(mun.op==MultUpdateNode.MODIFY))) {
+                               if (!interferes(update,r,dexpr.getExpr()))
+                                   continue; /* unique state - we're okay */
+                           }
                            if (interferes(un,update, r,dexpr))
                                return true;
                        }
@@ -209,6 +224,90 @@ class ConcreteInterferes {
        return false;
     }
 
+    private boolean interferes(Updates u, Rule r, Expr e) {
+       Set exprs=e.useDescriptor(u.getDescriptor());
+       for(Iterator eit=exprs.iterator();eit.hasNext();) {
+           Expr e2=(Expr)eit.next();
+           if (mayinterfere(u,r,e2))
+               return true;
+       }
+       return false;
+    }
+
+    private boolean mayinterfere(Updates u, Rule r, Expr e) {
+       // Note: rule of u must be r
+
+       Expr update_e=u.getLeftExpr();
+       HashSet quantifierset=new HashSet();
+
+       if (termination.analyzeQuantifiers(r,quantifierset))
+           return false; /* Can't accidentally interfere with other bindings if there aren't any! */
+
+       boolean firstfield=true;
+       while(true) {
+           if (update_e instanceof CastExpr)
+               update_e=((CastExpr)update_e).getExpr();
+           else if (e instanceof CastExpr)
+               e=((CastExpr)e).getExpr();
+           else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
+               DotExpr de1=(DotExpr)update_e;
+               DotExpr de2=(DotExpr)e;
+               if (de1.isValue()&&!firstfield)
+                   return true; /* Could have aliasing from this */
+               if (de1.getField()!=de2.getField())
+                   return true; /* Different fields: not comparible */
+               firstfield=false;
+
+               Expr index1=de1.getIndex();
+               Expr index2=de2.getIndex();
+               if (index1!=null) {
+                   assert index2!=null;
+                   if ((index1 instanceof VarExpr)&&(index2 instanceof VarExpr)) {
+                       VarDescriptor vd1=((VarExpr)index1).getVar();
+                       VarDescriptor vd2=((VarExpr)index2).getVar();
+                       if ((vd1==vd2)&&!vd1.isGlobal()) {
+                           quantifierset.add(getQuantifier(r,vd1));
+                           if (termination.analyzeQuantifiers(r,quantifierset))
+                               return false; /* State is disjoint from any other example */
+                       }
+                   }
+               }
+               update_e=de1.getExpr();
+               e=de2.getExpr();
+           } else if ((update_e instanceof VarExpr)&&(e instanceof VarExpr)) {
+               VarDescriptor vd1=((VarExpr)update_e).getVar();
+               VarDescriptor vd2=((VarExpr)e).getVar();
+               if ((vd1==vd2)&&!vd1.isGlobal()) {
+                   quantifierset.add(getQuantifier(r,vd1));
+                   if (termination.analyzeQuantifiers(r,quantifierset))
+                       return false; /* State is disjoint from any other example */
+               }
+               return true;
+           } else return true;
+       }
+
+    }
+
+    static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
+       for (int i=0;i<qs.numQuantifiers();i++) {
+           Quantifier q=qs.getQuantifier(i);
+           if (q instanceof SetQuantifier) {
+               SetQuantifier sq=(SetQuantifier)q;
+               if (sq.getVar()==vd)
+                   return sq;
+           } else if (q instanceof RelationQuantifier) {
+               RelationQuantifier rq=(RelationQuantifier)q;
+               if ((rq.x==vd)||(rq.y==vd))
+                   return rq;
+           } else if (q instanceof ForQuantifier) {
+               ForQuantifier fq=(ForQuantifier)q;
+               if (fq.getVar()==vd)
+                   return fq;
+           }
+       }
+       return null;
+    }
+    
     static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
        AbstractRepair ar=mun.getRepair();
        if (satisfy)

diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index 7ae89cb7143fc41e9b47a875ecae9da2eec0c7bc..192e212e6bd73e27d73f5933bd9a3f2df97cd824 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
@@ -179,6 +179,8 @@ public class ConstraintDependence {
                RelationInclusion ri=(RelationInclusion)r.getInclusion();
                Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
                SetDescriptor sd=e.getSet();
+               if (sd==null)
+                   sd=f.isInverse()?ri.getRelation().getRange():ri.getRelation().getDomain();
                if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
                    continue; /* This rule doesn't effect the function */
                if (foundrule) /* two different rules are a problem */

diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index 684c4fe364df7357468c96cb642af4ad2fafad1a..b0a49a3e8953dce5d42a1ccc7589da81b13995fb 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -67,6 +67,16 @@ public class DotExpr extends Expr {
        return name;
     }
     
+    public Set useDescriptor(Descriptor d) {
+       HashSet newset=new HashSet();
+       if (d==fd)
+           newset.add(this);
+       newset.addAll(left.useDescriptor(d));
+       if (intindex!=null)
+           newset.addAll(intindex.useDescriptor(d));
+       return newset;
+    }
+
     public boolean usesDescriptor(Descriptor d) {
        if (d==fd)
            return true;

diff --git a/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java b/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java
index 49b0064fd67a8c526b6c4624f72fcde69e892443..9630688fec8633768c1eb6ef8a894452c932cca2 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java
@@ -23,6 +23,14 @@ public class ElementOfExpr extends Expr {
            return true;
        return element.usesDescriptor(d);
     }
+    public Set useDescriptor(Descriptor d) {
+       HashSet newset=new HashSet();
+       if (d==set)
+           newset.add(this);
+       newset.addAll(element.useDescriptor(d));
+       return newset;
+    }
+
     public String name() {
        return element.name()+" in "+set.toString();
     }

diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index 771b9f8d8197194d5446db40631dda736eb0c44a..655004b4190edebf9711979dbdbb6372dc8fb225 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -53,6 +53,10 @@ public abstract class Expr {
        return false;
     }
 
+    public Set useDescriptor(Descriptor d) {
+       return new HashSet();
+    }
+
     public boolean usesDescriptor(Descriptor rd) {
        System.out.println(this.getClass().getName());
        throw new Error("UNIMPLEMENTED");
@@ -75,7 +79,7 @@ public abstract class Expr {
     }
 
     public SetDescriptor getSet() {
-       throw new Error("No Set for this Expr");
+       return null; /* unknown value */
     }
 
     public boolean isSafe() {

diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index 09895eb7eb58caeede387eac41dd59d9e974db86..89bc976ca1866a5a6afcbc240d214dd75f35d3f2 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -189,15 +189,17 @@ public class OpExpr extends Expr {
     }
 
     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 left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
-           //      return right.usesDescriptor(d);
-       else
-           return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
+       return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
     }
-    
 
+    public Set useDescriptor(Descriptor d) {
+       HashSet newset=new HashSet();
+       newset.addAll(left.useDescriptor(d));
+       if (right!=null)
+           newset.addAll(right.useDescriptor(d));
+       return newset;
+    }
+    
     public int[] getRepairs(boolean negated, Termination t) {
        if (left instanceof RelationExpr)
            return new int[] {AbstractRepair.MODIFYRELATION};

diff --git a/Repair/RepairCompiler/MCC/IR/RelationExpr.java b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
index 355f4619e0a6d35fb205ebb3d7e0009b64a03bc5..def95760ec410a02395af921ecd83525c7a797ed 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RelationExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
@@ -66,6 +66,14 @@ public class RelationExpr extends Expr {
        else
            return expr.usesDescriptor(rd);
     }
+
+    public Set useDescriptor(Descriptor rd) {
+       HashSet newset=new HashSet();
+       if (rd==relation)
+           newset.add(this);
+       newset.addAll(expr.useDescriptor(rd));
+       return newset;
+    }
     
     public RelationDescriptor getRelation() {
         return relation;

diff --git a/Repair/RepairCompiler/MCC/IR/SetExpr.java b/Repair/RepairCompiler/MCC/IR/SetExpr.java
index d50c50ea393bfc0a39ccb2766a6a320e8a4a001d..9deb8ac083cd343ce08662a1b599498edaf20a13 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SetExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/SetExpr.java
@@ -27,6 +27,13 @@ public class SetExpr extends Expr {
        return (s==sd);
     }
 
+    public Set useDescriptor(Descriptor s) {
+       HashSet newset=new HashSet();
+       if (s==sd)
+           newset.add(this);
+       return newset;
+    }
+
     public SetExpr() {
         this.sd = null;
     }

diff --git a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
index ec72e3fea6331ba72a8f5fbd03e5f8b631a94a6c..9cd29df41b158c48581cb1656b2600d737578516 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
@@ -33,6 +33,10 @@ public class SizeofExpr extends Expr {
        return setexpr.usesDescriptor(rd);
     }
 
+    public Set useDescriptor(Descriptor rd) {
+       return setexpr.useDescriptor(rd);
+    }
+
 
     public Descriptor getDescriptor() {
        return setexpr.getDescriptor();

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 830e07551e74c93ceb39d068260dbc1457811dd3..4698b51702b1b0f119a98f7130f0e482c8843c71 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -26,6 +26,7 @@ public class Termination {
     ComputeMaxSize maxsize;
     State state;
     AbstractInterferes abstractinterferes;
+    ConcreteInterferes concreteinterferes;
     ConstraintDependence constraintdependence;
     ExactSize exactsize;
     ArrayAnalysis arrayanalysis;
@@ -62,6 +63,7 @@ public class Termination {
        arrayanalysis=new ArrayAnalysis(state,this);
 
        abstractinterferes=new AbstractInterferes(this);
+       concreteinterferes=new ConcreteInterferes(this);
        generateconjunctionnodes();
        constraintdependence=new ConstraintDependence(state,this);
 
@@ -99,7 +101,6 @@ public class Termination {
            System.out.println("Can't generate terminating repair algorithm!");
            System.exit(-1);
        }
-       constraintdependence.traversedependences(this);
 
        System.out.println("Removing:");
        for(Iterator it=removedset.iterator();it.hasNext();) {
@@ -117,7 +118,7 @@ public class Termination {
            e.printStackTrace();
            System.exit(-1);
        }
-
+       constraintdependence.traversedependences(this);
     }
 
 
@@ -227,12 +228,12 @@ public class Termination {
            /* Cycle through the rules to look for possible conflicts */
            for(int i=0;i<state.vRules.size();i++) {
                Rule r=(Rule) state.vRules.get(i);  
-               if (ConcreteInterferes.interferes(mun,r,true)) {
+               if (concreteinterferes.interferes(mun,r,true)) {
                    GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
                    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
                    gn.addEdge(e);
                }
-               if (ConcreteInterferes.interferes(mun,r,false)) {
+               if (concreteinterferes.interferes(mun,r,false)) {
                    GraphNode scopenode=(GraphNode)scopefalsify.get(r);
                    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
                    gn.addEdge(e);
@@ -1092,4 +1093,25 @@ public class Termination {
        }
        return okay;
     }
+
+    public boolean analyzeQuantifiers(Quantifiers qs,Set set) {
+       for(int i=0;i<qs.numQuantifiers();i++) {
+           Quantifier q=qs.getQuantifier(i);
+           if (set.contains(q))
+               continue;
+           if (q instanceof SetQuantifier) {
+               SetDescriptor sd=((SetQuantifier)q).getSet();
+               if (maxsize.getsize(sd)<=1&&
+                   maxsize.getsize(sd)>=0)
+                   continue;
+           } else if (q instanceof RelationQuantifier) {
+               RelationDescriptor rd=((RelationQuantifier)q).getRelation();
+               if (maxsize.getsize(rd)<=1&&
+                   maxsize.getsize(rd)>=0)
+                   continue;
+           }
+           return false;
+       }
+       return true;
+    }
 }

diff --git a/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java b/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java
index 941b37a8f22b7ac2c2b168b15f1206fabd11a152..eabd01491b545008c63e7ff90d07598e94bcd9db 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java
@@ -39,6 +39,15 @@ public class TupleOfExpr extends Expr {
            return left.usesDescriptor(d)||right.usesDescriptor(d);
     }
 
+    public Set useDescriptor(Descriptor d) {
+       HashSet newset=new HashSet();
+       if (d==relation)
+           newset.add(this);
+       newset.addAll(left.useDescriptor(d));
+       newset.addAll(right.useDescriptor(d));
+       return newset;
+    }
+
     public boolean equals(Map remap, Expr e) {
        if (e==null||!(e instanceof TupleOfExpr))
            return false;

diff --git a/Repair/RepairCompiler/MCC/IR/VarExpr.java b/Repair/RepairCompiler/MCC/IR/VarExpr.java
index 00e83945355276480d4a9478081c615cab2a51bf..ddc0e8eb9b7de1c0c246de76ea57365502638614 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/VarExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/VarExpr.java
@@ -41,6 +41,13 @@ public class VarExpr extends Expr {
        return false;
     }
 
+    public Set useDescriptor(Descriptor d) {
+       HashSet newset=new HashSet();
+       if (d==vd)
+           newset.add(this);
+       return newset;
+    }
+
     public boolean isNonNull() {
        return true;
     }