Added code to compute maximum sizes of sets. So we can eliminate set removes

when they aren't necessary.

diff --git a/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java b/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java
new file mode 100755 (executable)
index 0000000..0dec8e0
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java
@@ -0,0 +1,80 @@
+package MCC.IR;
+import MCC.State;
+import java.util.*;
+
+/** This class computes the maximum size of sets and relations */
+
+public class ComputeMaxSize {
+    State state;
+    Hashtable sizemap; /* -1 means infinity */
+
+
+    public ComputeMaxSize(State state) {
+       this.state=state;
+       sizemap=new Hashtable();
+       computesizes();
+    }
+    
+    /** This method compute relation and set maximum sizes */
+    private void computesizes() {
+       Vector rules=state.vRules;
+       boolean change=true;
+       Set descriptorset=new HashSet();
+       descriptorset.addAll(state.stSets.getAllDescriptors());
+       descriptorset.addAll(state.stRelations.getAllDescriptors());
+       while(change) {
+           change=false;
+           for(Iterator dit=descriptorset.iterator();dit.hasNext();) {
+               Descriptor d=(Descriptor)dit.next();
+               if (d instanceof ReservedSetDescriptor)
+                   continue;
+               int totalsize=0;
+               for(int i=0;i<rules.size();i++) {
+                   Rule r=(Rule)rules.get(i);
+                   if (r.getInclusion().getTargetDescriptors().contains(d)) {
+                       /* This rule may add items to this set or relation */
+                       int rulesize=1;
+                       for(int j=0;j<r.numQuantifiers();j++) {
+                           Quantifier q=r.getQuantifier(j);
+                           int size=0;
+                           if (q instanceof RelationQuantifier) {
+                               Descriptor d2=((RelationQuantifier)q).getRelation();
+                               if (sizemap.containsKey(d2)) {
+                                   size=((Integer)sizemap.get(d2)).intValue();
+                               }
+                               if ((size!=0)&&(d==d2))
+                                   size=-1;
+                           } if (q instanceof SetQuantifier) {
+                               Descriptor d2=((SetQuantifier)q).getSet();
+                               if (sizemap.containsKey(d2)) {
+                                   size=((Integer)sizemap.get(d2)).intValue();
+                               }
+                               if ((size!=0)&&(d==d2))
+                                   size=-1;
+                           } else {
+                               size=-1;
+                           }
+                           if ((rulesize!=0)&&((size==-1)||(rulesize==-1)))
+                               rulesize=-1;
+                           else
+                               rulesize=rulesize*size;
+                       }
+                       
+                       if ((rulesize==-1)||(totalsize==-1))
+                           totalsize=-1;
+                       else
+                           totalsize+=rulesize;
+                   }
+               }
+               if (!sizemap.containsKey(d)||((Integer)sizemap.get(d)).intValue()!=totalsize) {
+                   change=true;
+                   sizemap.put(d,new Integer(totalsize));
+               }
+           }
+       }
+    }
+    int getsize(Descriptor d) {
+       return ((Integer)sizemap.get(d)).intValue();
+    }
+}
+

diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index 1e13217e4d85904234140fa3d71c29ea13d24307..e98abc530680eb0a66a66e1b4979368ee62ec05f 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -44,7 +44,7 @@ public abstract class Expr {
        return false;
     }
 
-    public int[] getRepairs(boolean negated) {
+    public int[] getRepairs(boolean negated, Termination t) {
        System.out.println(this.getClass().getName());
        throw new Error("Unrecognized EXPR");
     }

diff --git a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
index 4bed2313f7468f854b7fc2ffb7db3fab749ed9ef..762673236f256b18ab86169ac41ee35ce4bdf1ff 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
@@ -45,8 +45,8 @@ public class ExprPredicate extends Predicate {
         return expr.getInversedRelations();
     }
 
-    public int[] getRepairs(boolean negated) {
-       return expr.getRepairs(negated);
+    public int[] getRepairs(boolean negated, Termination t) {
+       return expr.getRepairs(negated,t);
     }
 
     public Descriptor getDescriptor() {

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 3bfefc026f602111140ef134b4cd804968f3b64c..e89898ab62dd372a5d02c6a083b023df6c156812 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -114,6 +114,13 @@ public class GraphAnalysis {
            for(Iterator it=cycles2.iterator();it.hasNext();) {
                GraphNode gn=(GraphNode)it.next();
                if (termination.conjunctions.contains(gn)) {
+                   try {
+                       GraphNode.DOTVisitor.visit(new FileOutputStream("graphdebug.dot"),cantremove);
+                   } catch (Exception e) {
+                       e.printStackTrace();
+                       System.exit(-1);
+                   }
+
                    System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
                    return null; // Out of luck
                }
@@ -230,13 +237,18 @@ public class GraphAnalysis {
            /* Searches scope nodes + compensation nodes */
            for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
                GraphNode gn=(GraphNode)it.next();
-               boolean foundcompensation=false;
+               int count=0;
                if (nodes.contains(gn)) {
                    for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
                        GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
                        GraphNode gn2=e.getTarget();
                        TermNode tn2=(TermNode)gn2.getOwner();
                        
+                       if ((tn2.getType()==TermNode.CONSEQUENCE)&&
+                           !mustremove.contains(gn2))
+                           count++;
+                           
+
                        if (tn2.getType()!=TermNode.UPDATE)
                            continue;
                        /* We have a compensation node */
@@ -253,22 +265,26 @@ public class GraphAnalysis {
                            }
                        } else {
                            if (!mustremove.contains(gn2))
-                               foundcompensation=true;
+                               count++;
                        }
                        if (!containsgn)
                            cantremove.remove(gn);
                        if (!containsgn2)
                            cantremove.remove(gn2);
                    }
-               }
-               if (!foundcompensation) {
-                   for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
-                       GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
-                       GraphNode gn2=e.getTarget();
-                       TermNode tn2=(TermNode)gn2.getOwner();
-                       if (tn2.getType()==TermNode.UPDATE) {
-                           cantremove.add(gn2);
-                           break;
+               
+                   if (count==1) {
+                       for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+                           GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+                           GraphNode gn2=e.getTarget();
+                           TermNode tn2=(TermNode)gn2.getOwner();
+                           if ((tn2.getType()==TermNode.UPDATE||tn2.getType()==TermNode.CONSEQUENCE)&&
+                               !mustremove.contains(gn2)) {
+                               if (!cantremove.contains(gn2)) {
+                                   cantremove.add(gn2);
+                                   change=true;
+                               }
+                           }
                        }
                    }
                }
@@ -297,6 +313,16 @@ public class GraphAnalysis {
                GraphNode gn=(GraphNode)it.next();
                System.out.println(gn.getTextLabel());
            }
+           System.out.println("Must remove set:");
+           for(Iterator it=mustremove.iterator();it.hasNext();) {
+               GraphNode gn=(GraphNode)it.next();
+               System.out.println(gn.getTextLabel());
+           }
+           System.out.println("Cant remove set:");
+           for(Iterator it=cantremove.iterator();it.hasNext();) {
+               GraphNode gn=(GraphNode)it.next();
+               System.out.println(gn.getTextLabel());
+           }
            
            
            while(true) {

diff --git a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
index c27bb443333a892ea706e7df02a418671d873b5a..8c4e6d1cf3273420c7f0cce838b33f87eff37f1b 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
@@ -56,7 +56,7 @@ public class InclusionPredicate extends Predicate {
            return setexpr.sd;
     }
 
-    public int[] getRepairs(boolean negated) {
+    public int[] getRepairs(boolean negated, Termination t) {
        if (setexpr instanceof ImageSetExpr) {
            if (negated)
                return new int[] {AbstractRepair.REMOVEFROMRELATION};

diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index c7cdd0d4cad9718e3f408a98ff314e63c902d556..4714735bd32e8c284a6538e9f53360433b76e102 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -178,7 +178,7 @@ public class OpExpr extends Expr {
     }
     
 
-    public int[] getRepairs(boolean negated) {
+    public int[] getRepairs(boolean negated, Termination t) {
        if (left instanceof RelationExpr)
            return new int[] {AbstractRepair.MODIFYRELATION};
        if (left instanceof SizeofExpr) {
@@ -199,35 +199,51 @@ public class OpExpr extends Expr {
                    op=Opcode.GT;
            }
 
+           int maxsize=t.maxsize.getsize(getDescriptor());
+           int size=getInt(right);
 
 
            boolean isRelation=((SizeofExpr)left).setexpr instanceof ImageSetExpr;
            if (isRelation) {
                if (op==Opcode.EQ) {
-                   if (((IntegerLiteralExpr)right).getValue()==0)
+                   if (size==0)
                        return new int[] {AbstractRepair.REMOVEFROMRELATION};
-                   else
+                   else {
+                       if ((maxsize!=-1)&&maxsize<=size)
+                           return new int[] {AbstractRepair.ADDTORELATION};
                        return new int[] {AbstractRepair.ADDTORELATION,
                                          AbstractRepair.REMOVEFROMRELATION};
+                   }
                } else if (op==Opcode.GE||op==Opcode.GT) {
                    return new int[]{AbstractRepair.ADDTORELATION}; 
                } else if (op==Opcode.LE||op==Opcode.LT) {
+                   if ((op==Opcode.LT&&maxsize!=-1&&maxsize<size)||(op==Opcode.LE&&maxsize!=-1&&maxsize<=size))
+                       return new int[0];
                    return new int[]{AbstractRepair.REMOVEFROMRELATION};
                } else if (op==Opcode.NE) {
+                   if (maxsize<size&&maxsize!=-1)
+                       return new int[0];
                    return new int[]{AbstractRepair.ADDTORELATION};
                } else throw new Error();
            } else {
                if (op==Opcode.EQ) {
-                   if (((IntegerLiteralExpr)right).getValue()==0)
+                   if (size==0)
                        return new int[] {AbstractRepair.REMOVEFROMSET};                        
-                   else
+                   else {
+                       if (maxsize<=size&&maxsize!=-1)
+                           return new int[] {AbstractRepair.ADDTOSET};
                        return new int[] {AbstractRepair.ADDTOSET,
                                              AbstractRepair.REMOVEFROMSET};
+                   }
                } else if (op==Opcode.GE||op==Opcode.GT) {
                    return new int[] {AbstractRepair.ADDTOSET}; 
                } else if (op==Opcode.LE||op==Opcode.LT) {
+                   if ((op==Opcode.LT&&maxsize<size&&maxsize!=-1)||(op==Opcode.LE&&maxsize<=size&&maxsize!=-1))
+                       return new int[0];
                    return new int[] {AbstractRepair.REMOVEFROMSET};
                } else if (op==Opcode.NE) {
+                   if (maxsize<size&&maxsize!=-1)
+                       return new int[0];
                    return new int[] {AbstractRepair.ADDTOSET};
                } else throw new Error();
            }

diff --git a/Repair/RepairCompiler/MCC/IR/Predicate.java b/Repair/RepairCompiler/MCC/IR/Predicate.java
index cb9aa39f56a3b2d33db1873243cee55fc0864662..be84d66a79a3e12c2ef73876080bbbf2c6bfa764 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Predicate.java
+++ b/Repair/RepairCompiler/MCC/IR/Predicate.java
@@ -7,7 +7,7 @@ public abstract class Predicate extends LogicStatement {
     public DNFConstraint constructDNF() {
        return new DNFConstraint(this);
     }
-    abstract public int[] getRepairs(boolean negated);
+    abstract public int[] getRepairs(boolean negated, Termination t);
     abstract public Descriptor getDescriptor();
     abstract public boolean inverted();
     public boolean usesDescriptor(RelationDescriptor rd) {

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index fe034f2be2e5ae930cdf0c860bdb039326072d4a..9d236e8cd469fea56f2b5ab90a78a508a6d365ac 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -1547,7 +1547,6 @@ public class RepairGenerator {
                }
            }
        }
-
        cr.endblock();
        cr.endblock();
     }

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 55f49522eb3b8d4d0ab834ffe628749282435816..73c89f10d8e7ceae652517c6e99c1f1f5c65e4a4 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -23,7 +23,7 @@ public class Termination {
     Hashtable conjtonodemap;
     Hashtable predtoabstractmap;
     Set removedset;
-
+    ComputeMaxSize maxsize;
     State state;
 
     public Termination(State state) {
@@ -45,6 +45,14 @@ public class Termination {
        if (!Compiler.REPAIR)
            return;
 
+       for(int i=0;i<state.vRules.size();i++)
+           System.out.println(state.vRules.get(i));
+       for(int i=0;i<state.vConstraints.size();i++)
+           System.out.println(state.vConstraints.get(i));
+
+
+       maxsize=new ComputeMaxSize(state);
+
        generateconjunctionnodes();
        generatescopenodes();
        generaterepairnodes();
@@ -264,7 +272,7 @@ public class Termination {
            Conjunction conj=tn.getConjunction();
            for(int i=0;i<conj.size();i++) {
                DNFPredicate dp=conj.get(i);
-               int[] array=dp.getPredicate().getRepairs(dp.isNegated());
+               int[] array=dp.getPredicate().getRepairs(dp.isNegated(),this);
                Descriptor d=dp.getPredicate().getDescriptor();
                for(int j=0;j<array.length;j++) {
                    AbstractRepair ar=new AbstractRepair(dp,array[j],d);