Improved precision of computation of maximum set sizes. Removed generation of
authorbdemsky <bdemsky>
Thu, 12 Aug 2004 21:41:40 +0000 (21:41 +0000)
committerbdemsky <bdemsky>
Thu, 12 Aug 2004 21:41:40 +0000 (21:41 +0000)
redundant rules by implicitschema.

Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java
Repair/RepairCompiler/MCC/IR/Expr.java
Repair/RepairCompiler/MCC/IR/ImplicitSchema.java

index 51221c3..a5a9d57 100755 (executable)
@@ -7,12 +7,14 @@ import java.util.*;
 public class ComputeMaxSize {
     State state;
     Hashtable sizemap; /* -1 means infinity */
-
+    static int KBOUND=100;
 
     public ComputeMaxSize(State state) {
        this.state=state;
        sizemap=new Hashtable();
        computesizes();
+       postprocess();
+       printsizes();
     }
     
     /** This method compute relation and set maximum sizes */
@@ -28,29 +30,42 @@ public class ComputeMaxSize {
                Descriptor d=(Descriptor)dit.next();
                if (d instanceof ReservedSetDescriptor)
                    continue;
-               int totalsize=0;
+               int totalstarts=0;
+               int totalchains=0;
+               Rule chainrule=null;
                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;
+                       boolean start=true;
                        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();
+                                   size=getsize(d2);
+                               }
+                               if (d==d2) {
+                                   if (!start)
+                                       size=-1;
+                                   else
+                                       size=1;
+                                   start=false;
                                }
-                               if ((size!=0)&&(d==d2))
-                                   size=-1;
                            } else if (q instanceof SetQuantifier) {
                                Descriptor d2=((SetQuantifier)q).getSet();
                                if (sizemap.containsKey(d2)) {
-                                   size=((Integer)sizemap.get(d2)).intValue();
+                                   size=getsize(d2);
+                               }
+                               if (d==d2) {
+                                   if (!start)
+                                       size=-1;
+                                   else
+                                       size=1;
+                                   start=false;
                                }
-                               if ((size!=0)&&(d==d2))
-                                   size=-1;
                            } else if (q instanceof ForQuantifier) {
                                ForQuantifier fq=(ForQuantifier)q;
                                boolean lowint=OpExpr.isInt(fq.lower);
@@ -60,30 +75,248 @@ public class ComputeMaxSize {
                                    if (size<=0) /* Catch sneaky bounds */
                                        throw new Error("Funny bounds in: "+fq);
                                } else size=-1;
-                           } else {
-                               size=-1;
-                           }
+                           } else 
+                               throw new Error("Unrecognized Quantifier");
+                           
                            if ((rulesize!=0)&&((size==-1)||(rulesize==-1)))
                                rulesize=-1;
                            else
                                rulesize=rulesize*size;
                        }
                        
-                       if ((rulesize==-1)||(totalsize==-1))
-                           totalsize=-1;
-                       else
-                           totalsize+=rulesize;
+                       if (start) {
+                           if ((rulesize==-1)||(totalstarts==-1))
+                               totalstarts=-1;
+                           else
+                               totalstarts+=rulesize;
+                       } else {
+                           if (totalchains==0)
+                               chainrule=r;
+                           else
+                               chainrule=null;
+                           if ((rulesize==-1)||(totalchains==-1))
+                               totalchains=-1;
+                           else
+                               totalchains+=rulesize;
+                       }
                    }
                }
-               if (!sizemap.containsKey(d)||((Integer)sizemap.get(d)).intValue()!=totalsize) {
+               if (totalstarts>=KBOUND)
+                   totalstarts=-1;
+               if (totalchains>=KBOUND)
+                   totalchains=-1;
+
+               if (!sizemap.containsKey(d)||getstarts(d)!=totalstarts||getchains(d)!=totalchains) {
                    change=true;
-                   sizemap.put(d,new Integer(totalsize));
+                   MaxSizeObject so=new MaxSizeObject(totalstarts,totalchains,chainrule);
+                   sizemap.put(d,so);
                }
            }
        }
     }
+
+    void printsizes() {
+       Set descriptorset=new HashSet();
+       descriptorset.addAll(state.stSets.getAllDescriptors());
+       descriptorset.addAll(state.stRelations.getAllDescriptors());
+       for(Iterator dit=descriptorset.iterator();dit.hasNext();) {
+           Descriptor d=(Descriptor)dit.next();
+           if (d instanceof ReservedSetDescriptor)
+               continue;
+           System.out.println("size("+d+")="+getsize(d));
+       }
+    }
+
+    private void postprocess() {
+       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 totalstarts=0;
+               int totalchains=0;
+               Rule chainrule=null;
+               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;
+                       boolean start=true;
+                       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=getsize(d2);
+                               }
+                               if (d==d2) {
+                                   if (!start)
+                                       size=-1;
+                                   else
+                                       size=1;
+                                   start=false;
+                               } else {
+                                   if (getchainrule(d2)!=null) {
+                                       if (isMutuallyExclusive(r, getchainrule(d2)))
+                                           size=getstarts(d2);
+                                   }
+                               }
+                           } else if (q instanceof SetQuantifier) {
+                               Descriptor d2=((SetQuantifier)q).getSet();
+                               if (sizemap.containsKey(d2)) {
+                                   size=getsize(d2);
+                               }
+                               if (d==d2) {
+                                   if (!start)
+                                       size=-1;
+                                   else
+                                       size=1;
+                                   start=false;
+                               } else {
+                                   if (getchainrule(d2)!=null) {
+                                       if (isMutuallyExclusive(r, getchainrule(d2)))
+                                           size=getstarts(d2);
+                                   }
+                               }
+                           } else if (q instanceof ForQuantifier) {
+                               ForQuantifier fq=(ForQuantifier)q;
+                               boolean lowint=OpExpr.isInt(fq.lower);
+                               boolean highint=OpExpr.isInt(fq.upper);
+                               if (lowint&&highint) {
+                                   size=1+OpExpr.getInt(fq.upper)-OpExpr.getInt(fq.lower);
+                                   if (size<=0) /* Catch sneaky bounds */
+                                       throw new Error("Funny bounds in: "+fq);
+                               } else size=-1;
+                           } else 
+                               throw new Error("Unrecognized Quantifier");
+                           
+                           if ((rulesize!=0)&&((size==-1)||(rulesize==-1)))
+                               rulesize=-1;
+                           else
+                               rulesize=rulesize*size;
+                       }
+                       
+                       if (start) {
+                           if ((rulesize==-1)||(totalstarts==-1))
+                               totalstarts=-1;
+                           else
+                               totalstarts+=rulesize;
+                       } else {
+                           if (totalchains==0)
+                               chainrule=r;
+                           else
+                               chainrule=null;
+                           if ((rulesize==-1)||(totalchains==-1))
+                               totalchains=-1;
+                           else
+                               totalchains+=rulesize;
+                       }
+                   }
+               }
+               if (totalstarts>=KBOUND)
+                   totalstarts=-1;
+               if (totalchains>=KBOUND)
+                   totalchains=-1;
+
+               if (!sizemap.containsKey(d)||getstarts(d)!=totalstarts||getchains(d)!=totalchains) {
+                   change=true;
+                   MaxSizeObject so=new MaxSizeObject(totalstarts,totalchains,chainrule);
+                   sizemap.put(d,so);
+               }
+           }
+       }
+
+    }
+
+    int getstarts(Descriptor d) {
+       MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+       return so.maxstarts;
+    }
+    int getchains(Descriptor d) {
+       MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+       return so.numberchains;
+    }
     int getsize(Descriptor d) {
-       return ((Integer)sizemap.get(d)).intValue();
+       MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+       if (so.maxstarts==0)
+           return 0;
+       if (so.numberchains!=0)
+           return -1;
+       return so.maxstarts;
     }
-}
 
+    private Rule getchainrule(Descriptor d) {
+       MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+       return so.chainrule;
+    }
+
+    public static boolean isMutuallyExclusive(Rule r1,Rule r2) {
+       // Building a map between quantifier variables
+       if (r1.numQuantifiers()!=r2.numQuantifiers())
+           return false;
+       Set usedDescriptors=new HashSet();
+       Hashtable varmap=new Hashtable();
+
+    outerloop:
+       for(int i=0;i<r1.numQuantifiers();i++) {
+           Quantifier q1=r1.getQuantifier(i);
+           if (!(q1 instanceof SetQuantifier))
+               return false;
+           if (usedDescriptors.contains(((SetQuantifier)q1).getSet()))
+               return false;
+           usedDescriptors.add(((SetQuantifier)q1).getSet());
+           for(int j=0;j<r2.numQuantifiers();j++) {
+               Quantifier q2=r2.getQuantifier(j);
+               if (!(q2 instanceof SetQuantifier))
+                   return false;
+               if (((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()) {
+                   varmap.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
+                   continue outerloop;
+               }
+           }
+           return false;
+       }
+       DNFRule dr1=r1.getDNFGuardExpr();
+       DNFRule dr2=r2.getDNFGuardExpr();
+       for(int i=0;i<dr1.size();i++) {
+           for(int j=0;j<dr2.size();j++) {
+               RuleConjunction rc1=dr1.get(i);
+               RuleConjunction rc2=dr2.get(j);
+               if (!exclusive(varmap,rc1,rc2))
+                   return false;
+           }
+       }
+       return true;
+    }
+    
+    private static boolean exclusive(Hashtable varmap, RuleConjunction rc1, RuleConjunction rc2) {
+       for (int i=0;i<rc1.size();i++) {
+           for (int j=0;j<rc2.size();j++) {
+               DNFExpr de1=rc1.get(i);
+               DNFExpr de2=rc2.get(j);
+               if ((de1.getNegation()!=de2.getNegation())&&
+                   (de1.getExpr().equals(varmap,de2.getExpr())))
+                   return true;
+           }
+       }
+       return false;
+    }
+}
+class MaxSizeObject {
+    int maxstarts;
+    int numberchains;
+    Rule chainrule;
+    
+    public MaxSizeObject(int start,int chain, Rule r) {
+       maxstarts=start;
+       numberchains=chain;
+       chainrule=r;
+    }
+}
index d45280d..51ae613 100755 (executable)
@@ -82,6 +82,13 @@ public abstract class Expr {
        return null; /* unknown value */
     }
 
+    public Expr stripCastExpr() {
+       Expr ptr=this;
+       while (ptr instanceof CastExpr)
+           ptr=((CastExpr)ptr).getExpr();
+       return ptr;
+    }
+
     public boolean isSafe() {
        return true;
     }
index 85bd076..f229334 100755 (executable)
@@ -338,6 +338,8 @@ public class ImplicitSchema {
     void updaterules() {
        Vector oldrules=state.vRules;
        Vector newrules=new Vector();
+       Vector allrules=new Vector();
+       allrules.addAll(oldrules);
        for(int i=0;i<oldrules.size();i++) {
            Rule r=(Rule)oldrules.get(i);
            if (r.inclusion instanceof SetInclusion) {
@@ -366,7 +368,9 @@ public class ImplicitSchema {
                                             this set, as item is already
                                             in this set. */
                        }
-                       
+                       if (isRedundant(allrules,r,sd1))
+                           continue;
+
                        Rule nr=new Rule();
                        nr.setGuardExpr(r.getGuardExpr());
                        nr.quantifiers=r.quantifiers;
@@ -377,6 +381,7 @@ public class ImplicitSchema {
                        nr.setnogenerate();
                        nr.num=r.num;
                        newrules.add(nr);
+                       allrules.add(nr);
                        state.implicitrule.put(nr,r);
                        if (!state.implicitruleinv.containsKey(r))
                            state.implicitruleinv.put(r,new HashSet());
@@ -386,4 +391,98 @@ public class ImplicitSchema {
        }
        oldrules.addAll(newrules);
     }
+
+    private boolean isRedundant(Vector allrules,Rule r,SetDescriptor sd) {
+    outerloop:
+       for(int i=0;i<allrules.size();i++) {
+           Rule r2=(Rule)allrules.get(i);
+           if (!(r2.getInclusion() instanceof SetInclusion))
+               continue;
+           //old rule to the same set as the new rule's inclusion condition
+           if (sd!=((SetInclusion)r2.getInclusion()).getSet())
+               continue;
+           //old rule quantifiers over superset of new rule's quantification
+           Hashtable varmap=buildvarmap(state,r2,r,true);
+           if (varmap==null)
+               continue;
+           Expr ei1=((SetInclusion)r.getInclusion()).getExpr();
+           Expr ei2=((SetInclusion)r2.getInclusion()).getExpr();
+           if (!ei2.stripCastExpr().equals(varmap,ei1.stripCastExpr())) //adds same expression
+               continue;
+           DNFRule dr1=r.getDNFGuardExpr();
+           DNFRule dr2=r2.getDNFGuardExpr();
+
+           //need to show that whenever the guard in r is satisfied, some guard in r2 is satisfied
+       innerloop1:
+           for(int j=0;j<dr1.size();j++) {
+               RuleConjunction rc1=dr1.get(j);
+           innerloop2:
+               for(int k=0;k<dr2.size();k++) {
+                   RuleConjunction rc2=dr2.get(k);
+                   //if rc1 being true implies rc2 being true continue to innerloop1
+               innerloop3:
+                   for(int l=0;l<rc2.size();l++) {
+                       DNFExpr de2=rc2.get(l);
+                       for(int m=0;m<rc1.size();m++) {
+                           DNFExpr de1=rc1.get(m);
+                           if (de1.getNegation()==de2.getNegation()&&
+                               de2.getExpr().equals(varmap,de1.getExpr()))
+                               continue innerloop3;
+                       }
+                       continue innerloop2; //see if we can satisfy some other conjunction
+                   }
+                   continue innerloop1; //all of the expr's in this conjunction are satisfied
+               }
+               continue outerloop;
+           }
+           return true;
+       }
+       return false;
+    }
+
+    public static Hashtable buildvarmap(State state,Rule r1,Rule r2,boolean subsetting) {
+       // Building a map between quantifier variables
+       Hashtable varmap=new Hashtable();
+       if (r1.numQuantifiers()!=r2.numQuantifiers())
+           return null;
+       Set usedQuantifiers=new HashSet();
+    outerloop:
+       for(int i=0;i<r1.numQuantifiers();i++) {
+           Quantifier q1=r1.getQuantifier(i);
+
+           if (q1 instanceof SetQuantifier) {
+               for(int j=0;j<r2.numQuantifiers();j++) {
+                   Quantifier q2=r2.getQuantifier(j);
+                   if (!(q2 instanceof SetQuantifier))
+                       continue;;
+                   if (usedQuantifiers.contains(q2))
+                       continue;
+                   if (((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()||
+                       (subsetting&&((SetQuantifier)q1).getSet().isSubset(((SetQuantifier)q2).getSet()))) {
+                       varmap.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
+                       usedQuantifiers.add(q2);
+                       continue outerloop;
+                   }
+               }
+               return null;
+           } else if (q1 instanceof RelationQuantifier) {
+               for(int j=0;j<r2.numQuantifiers();j++) {
+                   Quantifier q2=r2.getQuantifier(j);
+                   if (!(q2 instanceof RelationQuantifier))
+                       continue;
+                   if (usedQuantifiers.contains(q2))
+                       continue;
+                   if (((RelationQuantifier)q1).getRelation()==((RelationQuantifier)q2).getRelation()) {
+                       varmap.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
+                       varmap.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
+                       usedQuantifiers.add(q2);
+                       continue outerloop;
+                   }
+               }
+               return null;
+           }
+       }
+       return varmap;
+    }
+
 }